Verification via Structure Simulation
作者： Niel Immerman , Alexander Rabinovich , Thomas W. Reps , Mooly Sagiv , Great Yorsh
DOI: 10.1007/978-3-540-27813-9_22
关键词:
摘要: This paper shows how to harness decision procedures automatically verify safety properties of imperative programs that perform dynamic storage allocation and destructive updating structure fields. Decidable logics can express reachability are used state linked data structures, while guaranteeing the verification method always terminates. The main technical contribution is a simulation in which set original structures we wish model, e.g., doubly lists, nested binary trees, etc., mapped tractable be reasoned about using decidable logics. rather limited they directly model. For instance, our examples use logic MSO-E, only model function graphs; however, technique provides an indirect way additional structures.
springer.com
core.ac.uk
sci-hub.st 参考文章(16)
Neil Immerman, Alex Rabinovich, Tom Reps, Mooly Sagiv, Greta Yorsh, None, The Boundary Between Decidability and Undecidability for Transitive-Closure Logics computer science logic. ,vol. 3210, pp. 160- 174 ,(2004) , 10.1007/978-3-540-30124-0_15
Thomas Reps, Mooly Sagiv, Greta Yorsh, Symbolic Implementation of the Best Transformer verification model checking and abstract interpretation. pp. 252- 266 ,(2004) , 10.1007/978-3-540-24622-0_21
G. Yorsh, Thomas Reps, Mooly Sagiv, Symbolically Computing Most-Precise Abstract Operations for Shape Analysis tools and algorithms for construction and analysis of systems. pp. 530- 545 ,(2004) , 10.1007/978-3-540-24730-2_39
Jesper G. Henriksen, Jakob Jensen, Michael Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, Anders Sandholm, Mona: Monadic Second-Order Logic in Practice tools and algorithms for construction and analysis of systems. pp. 89- 110 ,(1995) , 10.1007/3-540-60630-0_5
Michael Benedikt, Thomas Reps, Mooly Sagiv, A Decidable Logic for Describing Linked Data Structures european symposium on programming. pp. 2- 19 ,(1999) , 10.1007/3-540-49099-X_2
Anders Møller, Michael I. Schwartzbach, The pointer assertion logic engine Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation - PLDI '01. ,vol. 36, pp. 221- 231 ,(2001) , 10.1145/378795.378851
Patrick Cousot, Radhia Cousot, Systematic design of program analysis frameworks symposium on principles of programming languages. pp. 269- 282 ,(1979) , 10.1145/567752.567778
L.J. Hendren, A. Nicolau, Parallelizing programs with recursive data structures IEEE Transactions on Parallel and Distributed Systems. ,vol. 1, pp. 35- 47 ,(1990) , 10.1109/71.80123
C. A. R. Hoare, Recursive data structures International Journal of Parallel Programming. ,vol. 4, pp. 105- 132 ,(1975) , 10.1007/BF00976239
Mooly Sagiv, Thomas Reps, Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating ACM Transactions on Programming Languages and Systems. ,vol. 20, pp. 1- 50 ,(1998) , 10.1145/271510.271517