Lazy abstraction

ABSTRACT

One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, refine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-refine loop. Lazy abstraction continuously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs. We also provide sufficient conditions for the termination of the method.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 3: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 4: Thomas Ball , Andreas Podelski , Sriram K. Rajamani, Boolean and Cartesian Abstraction for Model Checking C Programs, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.268-283, April 02-06, 2001
• 5: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 6: D. Blei etal. Vampyre: A proof generating theorem prover. http://www.eees.berkeley.edu/rupak/Vampyre.
• 7: Bernard Boigelot , Patrice Godefroid, Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs (Extended Abstract), Proceedings of the 8th International Conference on Computer Aided Verification, p.1-12, August 03, 1996
• 8: Bernard Boigelot , Pierre Wolper, Symbolic Verification with Periodic Sets, Proceedings of the 6th International Conference on Computer Aided Verification, p.55-67, June 21-23, 1994
• 9: Ahmed Bouajjani , Peter Habermehl, Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations, Theoretical Computer Science, v.221 n.1-2, p.211-250, June 28, 1999 [doi>10.1016/S0304-3975(99)00033-X]
• 10: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 11: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 12: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• 13: Satyaki Das , David L. Dill, Successive Approximation of Abstract Transition Relations, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.51, June 16-19, 2001
• 14: Giorgio Delzanno , Andreas Podelski, Model Checking in CLP, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.223-239, March 22-28, 1999
• 15: D. Detlefs, G. Nelson, and J. Saxe. Simplify theorem prover. http://researeh.eompaq.eom/SRC/ese/Simplify.html.
• 16: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 17: D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI 00: Operating System Design and Implementation. Usenix Association, 2000.
• 18: Alain Finkel , S. Purushothaman Iyer , Grégoire Sutre, Well-Abstracted Transition Systems, Proceedings of the 11th International Conference on Concurrency Theory, p.566-580, August 22-25, 2000
• 19: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-Sensitive Type Qualifiers, University of California at Berkeley, Berkeley, CA, 2001
• 20: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 21: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 22: Thomas A. Henzinger , Rupak Majumdar, A Classification of Symbolic Transition Systems, Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, p.13-34, February 01, 2000
• 23: C. Linet al. C-breeze: C compiler infrastructure. http://www.es.utexas.edu/users/e-breeze.
• 24: J.M. Morris. A general axiom of assignment. In Theoretical Foundations of Programming Methodology, International Summer School, pp. 25-34. Reidel, 1982.
• 25: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 26: G. Nelson. Techniques for Program Verification. Technical Report CSL81-10, Xerox Palo Alto Research Center, 1981.
• 27: Sam Owre , S. Rajan , John M. Rushby , Natarajan Shankar , Mandayam K. Srivas, PVS: Combining Specification, Proof Checking, and Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.411-414, August 03, 1996
• 28: Hassen Saïdi, Model Checking Guided Abstraction and Analysis, Proceedings of the 7th International Symposium on Static Analysis, p.377-396, June 29-July 01, 2000
• 29: F. Somenzi. Colorado university decision diagram package, http://vlsi.eolorado.edu/pub, 1998.
• 30: N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter 1993 Technical Conference, pp. 977-106, 1993.