Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures
Open Access
- 1 January 2005
- conference paper
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 99-115
- https://doi.org/10.1007/11532231_8
Abstract
No abstract availableThis publication has 22 references indexed in Scilit:
- The Boundary Between Decidability and Undecidability for Transitive-Closure LogicsLecture Notes in Computer Science, 2004
- Static Program Analysis via 3-Valued LogicLecture Notes in Computer Science, 2004
- Transitive Closure and the Mechanization of MathematicsApplied Logic Series, 2003
- Extended static checking for JavaPublished by Association for Computing Machinery (ACM) ,2002
- The pointer assertion logic enginePublished by Association for Computing Machinery (ACM) ,2001
- TVLA: A System for Implementing Static AnalysesLecture Notes in Computer Science, 2000
- Undecidability results on two-variable logicsArchive for Mathematical Logic, 1999
- SPASS & FLOTTER version 0.42Lecture Notes in Computer Science, 1996
- Verifying reachability invariants of linked structuresPublished by Association for Computing Machinery (ACM) ,1983
- Recursive data structuresInternational Journal of Parallel Programming, 1975