Introduction to CEGAR —Counter-Example Guided Abstraction Refinement
Abstract
Precision, completeness and scalability of static verification tools have dramatically improved over the last decade. In particular, automatic checking of moderate-sized software systems has been made possible due to development of CEGAR — Counter-Example Guided Abstraction Refinement. This approach is used in such tools as SLAM, BLAST, SATABS, and CPAchecker. The paper presents an extended review of predicate abstraction-based CEGAR. It provides an introduction to the general principles of CEGAR and describes some implementation details of CEGAR in BLAST and CPAchecker. In particular, the paper concerns deciding the reachability problem for C programs by means of symbolic predicate abstraction. The set of predicates for the abstraction is obtained by Craig interpolation of the logical formulas representing the counterexample traces being discovered during the analysis. This technique is explained by two examples analyzed step-by-step both in intuitive and in formal manner. The explanation proceeds from a number of greatly simplified programs employing a very restricted subset of C language features (e.g. using only a finite set of integer variables) to more complicated programs of arbitrary size with pointers, heap allocations and bit operations. In terms of considered abstract domains the paper describes the simplest fine-grained Cartesian abstraction and a coarse-grained Boolean abstraction with adjustable block encoding. The paper also includes small discussions on common issues arising from verification of real industrial C codebase and current capabilities of existing decision procedure implementations.
About the Authors
M. U. Mandrykin
ISP RAS, Moscow
Russian Federation
Russian Federation
V. S. Mutilin
ISP RAS, Moscow
Russian Federation
Russian Federation
A. V. Khoroshilov
ISP RAS, Moscow
Russian Federation
Russian Federation
References
1. Dershowitz N. Software horror stories. URL: http://www.cs.tau.ac.il/~nachumd/horror.html
2. Turing A. M. On Computable numbers, with an application to the Entscheidungsproblem. In Proc. London Mathematical Society, pp. 230—265, 1936.
3. Floyd R. Assigning Meanings to Programs. Mathematical Aspects of Computer Science, pp. 19—32, 1967.
4. Hoare C. An Axiomatic Basis for Computer Programming. Communications of the ACM (CACM), vol. 12, issue 10, pp. 576-580, 1969. doi: 10.1145/363235.363259
5. Dijkstra E. A Discipline of Programming. Prentice-Hall, 1976.
6. [6]. Millo R. D., Lipton R., Perlis A. Social Processes and Proofs of Theorems and Programs. Communications of the ACM (CACM ),vol. 22, issue 5, pp. 271-280, 1979. doi: 10.1145/359104.359106
7. Nelson G. Techniques for Program Verification. Technical Report CSL81-10: Xerox Palo Alto Research Center, 1981.
8. Nelson G., Oppen D. Fast Decision Procedures Based on Congruence Closure. Journal of the ACM (JACM), vol. 27. pp. 356-364, 1980.
9. Shostak R. Deciding Combinations of Theories. LNCS, vol. 138, pp. 209-222, 1982. doi: 10.1007/BFb0000061
10. Clarke E. M., Emerson E. A. Synthesis of Synchronization Skeletons for Branching Time Temporal. LNCS, vol. 131, pp. 52-71, 1982. doi: 10.1007/BFb0025774
11. Queille J., Sifakis J. Specification and Verification of Concurrent Systems in Cesar. In Proc. of 5th International Symposium on Programming, LNCS, vol. 137, pp. 337-351, 1981. doi: 10.1007/3-540-11494-7_22
12. Vardi M., Wolper P. Reasoning about Infinite Computations. Information and Computation, vol. 115, issue 1, pp. 1–37, 1994. doi: 10.1006/inco.1994.1092
13. Pnueli A. The Temporal Logic of Programs. In Proc. 18th Annual Symposium on Foundations of Computer Science, pp. 46-57, 1977. doi: 10.1109/SFCS.1977.32
14. Emerson E. Temporal and Modal Logic. Handbook of Theoretical Computer Science. Elsevier Science Publishers, vol. B, pp. 995-1072, 1990.
15. Khedker U. P., Sanyal A., Karkare B. Data Flow Analysis: Theory and Practice. CRC Press (Taylor and Francis Group), 2009.
16. D'Silva V., Kroening D., Weissenbacher G. A Survey of Automated Techniques for Formal Software Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), vol. 27, issue 7, pp. 1165-1178, 2009. doi: 10.1109/TCAD.2008.923410
17. Jhala R., Majumdar R. Software model checking. ACM Computing Surveys (CSUR), vol. 41, issue 4, article 21, 2009. doi: 10.1145/1592434.1592438
18. Beyer D. Petrenko A. Linux Driver Verification. In Proc. Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies, LNCS, vol. 7610, pp. 1-6, 2012. doi: 10.1007/s10009-007-0044-z
19. Nesov V. Automatically Finding Bugs in Open Source Programs. Third International Workshop on Foundations and Techniques for Open Source Software Certification, OpenCert 2009, vol. 20, pp.19-29, 2009.
20. Engler D., Chelf B., Chou A., Hallem S. Checking system rules using system-specific, programmer-written compiler extensions. In Proc. 4th conference on Symposium on Operating System Design & Implementation (OSDI), vol. 4, pp. 1-16, 2000.
21. Lawall J. L., Brunel J., Palix N., Rydhof H. R., Stuart H., Muller G. WYSIWIB: A declarative approach to finding API protocols and bugs in Linux code. In Proc. 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 43—52, 2009.
22. Avetisyan A., Borodin A. Mekhanizmy rasshireniya sistemy staticheskogo analiza Svace detektorami novykh vidov uyazvimostej i kriticheskikh oshibok [Mechanisms for extending the system of static analysis Svace by new types of detectors of vulnerabilities and critical errors]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 21, pp. 39-54, 2011 (in Russian).
23. Ignatyev V.N. Ispol'zovanie legkovesnogo staticheskogo analiza dlya proverki nastraivaemykh semanticheskikh ogranichenij yazyka programmirovaniya [Using static analysis for checking configurable semantic restrictions on a programming language]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 22, pp. 169-188, 2012 (in Russian).
24. Biere A., Cimatti A, Clarke E., Strichman O., Zhu Y. Bounded model checking. Advances in Computers, vol. 58, 2003.
25. Clarke E., Grumberg O., Jha S., Lu Y., Veith H. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM (JACM), vol. 50, issue 5, pp. 752-794, 2003. doi: 10.1145/876638.876643
26. Thomas D., Moorby P. The Verilog Hardware Description Language. Kluwer Academic Publishers, 1998.
27. Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 2988, pp. 168-176, 2004. doi: 10.1007/978-3-540-24730-2_15
28. Ivancic F., Yang Z., Ganai M.K., Gupta A., Shlyakhter I., Ashar P. F-soft: Software verification platform. In Proc. Computer Aided Verification (CAV), LNCS, vol. 3576, pp. 301-306, 2005. doi: 10.1007/11513988_31
29. Post H., Sinz C., Merz F., Gorges T., Kropf T. Linking functional requirements and software verification. In Proc. 17th IEEE International Requirements Engineering Conference, pp. 295-302, 2009. doi: 10.1109/RE.2009.43
30. Donaldson A. F., Kroening D., Ruemmer P. Automatic analysis of DMA races using model checking and k-induction. Formal Methods in System Design, vol. 39, pp. 83-113, 2011. doi: 10.1007/s10703-011-0124-2
31. Ball T., Bounimova E., Levin V., Kumar R., Lichtenberg J. The Static Driver Verifier Research Platform. Computer Aided Verification (CAV), LNCS, vol. 6174, pp. 119-122, 2010. doi: 10.1007/978-3-642-14295-6_11
32. Beyer D., Henzinger T., Jhala R., Majumdar R. The Software Model Checker Blast: Applications to Software Engineering. Int. Journal on Software Tools for Technology Transfer (STTT), vol. 5, pp. 505-525, 2007. doi: 10.1007/s10009-007-0044-z
33. Clarke E., Kroening D., Sharygina N., Yorav K. SATABS: SAT-based Predicate Abstraction for ANSI-C. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 3440, pp. 570-574, 2005. doi: 10.1007/978-3-540-31980-1_40
34. Beyer D., Keremoglu M.E. CPAchecker: A Tool for Configurable Software Verification. In Proc. Computer Aided Verification (CAV), LNCS, vol. 6806, pp. 184–190, 2011. 10.1007/978-3-642-22110-1_16
35. Mutilin V.S., Novikov E.M., Strakh А.V., Khoroshilov А.V., Shved P.E. Аrkhitektura Linux Driver Verification [Linux Driver Verification Architecture]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 20, pp. 163-187, 2011 (in Russian).
36. Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A. Towards an Open Framework for C Verification Tools Benchmarking. In Proc. Perspectives of Systems Informatics (PSI), LNCS, vol. 7162, pp. 82-91, 2012. doi: 10.1007/978-3-642-29709-0_17
37. Graf S., Saidi H. Construction of Abstract State Graphs with PVS. In Proc. Computer Aided Verification (CAV), LNCS, vol. 1254, pp. 72-83, 1997. doi: 10.1007/3-540-63166-6_10
38. Henzinger T.A., Jhala, R., Majumdar, R., Sutre, G. Lazy abstraction. In Proc. 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), Pages 58-70, 2002. doi: 10.1145/503272
39. Cytron R., Ferrante J., Rosen B.K.,Wegman M.N., Zadek F.K. Efficiently computing static single-assignment form and the program dependence graph. ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 13, issue 4, pp. 451-490, 1991. doi: 10.1145/115372.115320
40. Craig W. Linear reasoning. Symbolic Logic, vol. 22, pp. 250–268, 1957.
41.
42. Henzinger T.A., Jhala R., Majumdar R., McMillan K.L. Abstractions from proofs. In Proc. 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), pp. 232-244, 2004. doi: 10.1145/964001.964021
43. Beyer D., Cimatti A., Griggio A., Keremoglu M.E., Sebastiani R. Software Model Checking via Large-Block Encoding. In Proc. Formal Methods in Computer-Aided Design (FMCAD), pp. 25–32, 2009. doi: 10.1109/FMCAD.2009.5351147
44. Beyer D., Keremoglu M. E., Wendler P. Predicate abstraction with adjustable-block encoding. In Proc. Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 189-198, 2010.
45. Berndl M., Lhotak O., Qian F., Hendren L., Umanee N. Points-to analysis using BDDs. Proc. ACM SIGPLAN conference on Programming language design and implementation (PLDI), pp. 103 – 114, 2003. doi: 10.1145/781131.781144
46. George C. Necula, Scott McPeak, S. P. Rahul, Westley Weimer. CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In Proc. Conference on Compiler Construction, LNCS, vol. 2304, pp. 213-228, 2002. doi: 10.1007/3-540-45937-5_16
47. Nori A.V., Rajamani S.K. An Empirical Study of Optimizations in Yogi. In Proc. 32nd ACM/IEEE International Conference on Software Engineering (ICSE), vol. 1, pp. 355-364, 2010. doi: 10.1145/1806799.1806852
48. Cimatti A., Griggio A., Joost S. B., Sebastiani R. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7795, pp. 93—107, 2013.doi: 10.1007/978-3-642-36742-7_7
49. Nieuwenhuis R., Rubio A. Paramodulation-Based Theorem Proving. Handbook of Automated Reasoning, Elsevier Science and MIT Press, 2001.
50. Kroening D., Strichman O. Decision Procedures: An Algorithmic Point of View. Journal of Automated Reasoning, vol. 51, issue 4, pp. 453-456, 2008. doi: 10.1007/s10817-013-9295-4
51. Bozzano M., Bruttomesso R., Cimatti A., Junttila T., Ranise S., Van Rossum P., Sebastiani R. Efficient Satisfiability Modulo Theories via Delayed Theory Combination. In Proc. Computer Aided Verification (CAV), LNCS, vol. 3576, pp. 335-349, 2005. doi: 10.1007/11513988_34
52. Yorsh G., Musuvathi M. A Combination Method for Generating Interpolants. In Proc. Conference on Automated Deduction (CADE), LNCS, vol. 3632, pp. 353-368, 2005. doi: 10.1007/11532231_26
53. Rybalchenko A., Sofronie-Stokkermans V. Constraint Solving for Interpolation. In Proc. Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, vol. 4349, pp. 346-362, 2007. doi: 10.1007/978-3-540-69738-1_25
54. McMillan K. L. An Interpolating Theorem Prover. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 2988, pp 16-30, 2004. doi : 10.1007/978-3-540-24730-2_2
55. Beyer D., Zufferey D., Majumdar R. CSIsat: Interpolation for LA+EUF. In Proc. Computer Aided Verification (CAV), LNCS, vol. 5123, pp. 304-308, 2008. doi: 10.1007/978-3-540-70545-1_29
56. Cimatti A., Griggio A., Sebastiani R. Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories. ACM Transactions on Computational Logic (TOCL), vol. 12, issue 1, 2010. doi: 10.1145/1838552.1838559
57. Thi Thieu Hoa Le. A Novel Technique for Computing Craig Interpolants in Satisfiabilility modulo the Theory of Integer Linear Arithmetic. PhD thesis, 2010.
58. De Moura L., Bjorner N. Z3: an efficient SMT solver. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 4963, pp. 337-340, 2008. doi: 10.1007/978-3-540-78800-3_24
59. Ball T., Bounimova E., Kumar R., Levin V. SLAM2: Static Driver Verification with Under 4% False Alarms. In Proc. Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 35-42, 2010.
60. Beyer D. Competition on Software Verification. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp. 504-524, 2012. doi: 10.1007/978-3-642-28756-5_38
61. Beyer D. Second Competition on Software Verification. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 7214, pp 504-524, 2012. doi: 10.1007/978-3-642-28756-5_38
62. Cimatti A., Micheli A., Narasamdya I., Roveri M. Verifying SystemC: A Software Model Checking Approach. In Proc. Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 51–59, 2010.
63. Galloway A., Lüttgen G., Mühlberg J.T., Siminiceanu R.I. Model-Checking the Linux Virtual File System. In Proc. Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol. 5403, pp. 74—88, 2009. doi: 10.1007/978-3-540-93900-9_10
64. Mühlberg J.T., Lüttgen G. Blasting Linux Code. In Proc. Formal Methods: Applications and Technology, LNCS, vol. 4346, pp. 211—226, 2007. doi: 10.1007/978-3-540-70952-7_14
65. Penninckx W., Mühlberg J. T., Smans J., Jacobs B., Piessens F. Sound Formal Verification of Linux’s USB BP Keyboard Driver. NASA Formal Methods, LNCS, vol. 7226, pp. 210-215, 2012. doi: 10.1007/978-3-642-28891-3_21
66. Apel S., Speidel H., Wendler P., von Rhein A., Beyer D. Detection of feature interactions using feature-aware verification. In Proc. IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 372-375, 2011. doi: 10.1109/ASE.2011.6100075
67. Classen A., Heymans P., Schobbens P.-Y., Legay A. Symbolic model checking of software product lines. In Proc. International Conference on Software Engineering (ICSE), pp. 321-330, 2011. doi: 10.1145/1985793.1985838
68. Beyer D., Henzinger T. A., Theoduloz G. Program Analysis with Dynamic Precision Adjustment. In Proc. IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 29-38, 2008. doi: 10.1109/ASE.2008.13
69. Cousot P., Cousot R., Feret J., Mauborgne L., Miné A., Monniaux D., Rival X. Combination of Abstractions in the ASTREE Static Analyzer. In Proc. Advances in Computer Science (ASIAN), LNCS, vol. 4435, pp. 272-300, 2007. doi: 10.1007/978-3-540-77505-8_23
70. Corbet J., Rubini A., Kroah-Hartman G. Linux Device Drivers. O'Reilly Media, pp. 58—59, 2005.
Review
For citations:
Mandrykin M.U., Mutilin V.S., Khoroshilov A.V. Introduction to CEGAR —Counter-Example Guided Abstraction Refinement. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2013;24. (In Russ.)
Email this article 