An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
- 12 November 2007
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC
Abstract
No abstract availableKeywords
This publication has 23 references indexed in Scilit:
- Interprocedural Shape Analysis with Separated Heap AbstractionsLecture Notes in Computer Science, 2006
- A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating ProgramsLecture Notes in Computer Science, 2005
- Field Constraint AnalysisLecture Notes in Computer Science, 2005
- Abstract State Machines 2004. Advances in Theory and PracticePublished by Springer Science and Business Media LLC ,2004
- Predicate abstraction for software verificationPublished by Association for Computing Machinery (ACM) ,2002
- Lazy abstractionPublished by Association for Computing Machinery (ACM) ,2002
- A Decidable Logic for Describing Linked Data StructuresLecture Notes in Computer Science, 1999
- Experience with Predicate AbstractionLecture Notes in Computer Science, 1999
- Verifying reachability invariants of linked structuresPublished by Association for Computing Machinery (ACM) ,1983
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpointsPublished by Association for Computing Machinery (ACM) ,1977