Введение в метод CEGAR - уточнение абстракции по контрпримерам
Аннотация
Точность, полнота и масштабируемость применяемых на практике инструментов статической верификации значительно возросла за последнее десятилетие. В частности, успешный автоматизированный анализ программных систем среднего размера с использованием проверки моделей, получаемых при помощи предикатной абстракции, стал возможен благодаря развитию метода уточнения абстракции по контрпримерам - CEGAR (Counter Example Guided Abstraction Refinement). Этот метод так или иначе используется в таких инструментах, как SLAM, BLAST, SATABS и CPAchecker. В рамках данной статьи мы рассмотрим метод CEGAR в том виде, как он реализован в инструментах статической верификации BLAST и CPAchecker.
Об авторах
М. У. Мандрыкин
ИСП РАН
Россия
Россия
В. С. Мутилин
ИСП РАН
Россия
Россия
А. В. Хорошилов
ИСП РАН
Россия
Россия
Список литературы
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 // Proceedings of the London Mathematical Society. 1936. pp. 230—265.
3. Floyd R. Assigning Meanings to Programs // Mathematical Aspects of Computer Science. 1967. pp. 19—32.
4. Hoare C. An Axiomatic Basis for Computer Programming // Communications of the ACM. 1969. vol. 12. pp. 576—580.
5. Dijkstra E. A Discipline of Programming // Prentice-Hall, 1976.
6. Millo R. D., Lipton R., Perlis A. Social Processes and Proofs of Theorems and Programs // Communications of the ACM. 1979. vol. 22. pp.271—280.
7. Nelson G. Techniques for Program Verification // Tech. Rep. CSL81-10: Xerox Palo Alto Research Center, 1981.
8. Nelson G., Oppen D. Fast Decision Procedures Based on Congruence Closure // Journal of the ACM. 1980. vol. 27. pp. 356—364.
9. Shostak R. Deciding Combinations of Theories // Journal of the ACM. 1984. vol. 31. pp. 1—12.
10. Clarke E. M., Emerson E. A. Synthesis of Synchronization Skeletons for Branching Time Temporal Logic // Logic of Programs. 1981. vol. 131. pp. 52—71.
11. Queille J., Sifakis J. Specification and Verification of Concurrent Systems in Cesar // Fifth International Symposium on Programming / Ed. by M. Dezani-Ciancaglini, U. Montanari. Lecture Notes in Computer Science. Springer-Verlag, 1981. pp. 337—351.
12. Vardi M., Wolper P. Reasoning about Infinite Computations // Information and Computation. 1994. vol. 115. pp. 1—37.
13. Pnueli A. The Temporal Logic of Programs // Proceedings of the 18th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, 1977. pp. 46—57.
14. Emerson E. Temporal and Modal Logic // Handbook of Theoretical Computer Science / Ed. by J. van Leeuwen. Elsevier Science Publishers, 1990. vol. B. pp. 995—1072.
15. Khedker Uday P., Sanyal Amitabha, Karkare Bageshri. 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 // Computer-Aided Design of Integrated Circuits and Systems. 2008. vol. 27, no. 7. pp. 1165—1178. On IEEE Transactions.
17. Jhala R., Majumdar R. Software model cheking // ACM Computing Surveys. 2009.
18. Д. Бейер, А.К. Петренко. Верификация драйверов операционной системы Linux // Труды Института системного программирования РАН, том 23, ISSN 2220-6426 (Online), ISSN 2079-8156 (Print), 2012 г. cтр. 405-412.
19. Vladimir Nesov. Automatically Finding Bugs in Open Source Programs // Third International Workshop on Foundations and Techniques for Open Source Software Certification. OpenCert 2009 vol. 20 2009. pp.19—29.
20. Dawson Engler, Benjamin Chelf, Andy Chou. Checking system rules using system-specific, programmer-written compiler extensions // Proceedings of the 4th conference on Symposium on Operating System Design & Implementation vol. 4 OSDI'00. 2000.
21. pp. 1—16.
22. Julia L. Lawall, Julien Brunel, Nicolas Palix, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller. WYSIWIB: A declarative approach to finding API protocols and bugs in Linux code // DSN'09 – The 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks. 2009. pp. 43—52.
23. Арутюн Аветисян, Алексей Бородин. Механизмы расширения системы статического анализа Svace детекторами новых видов уязвимостей и критических ошибок // Труды Института системного программирования РАН, том 21, ISSN 2220-6426 (Online), ISSN 2079-8156 (Print). 2011. стр. 39-54.
24. В.Н. Игнатьев. Использование легковесного статического анализа для проверки настраиваемых семантических ограничений языка программирования // Труды Института системного программирования РАН, том 22, ISSN 2220-6426 (Online), ISSN 2079-8156 (Print). 2012. стр. 169-188.
25. Biere A., Cimatti A, Clarke E., Strichman O., Zhu Y. Bounded model checking // Advances in Computers. 2003.
26. Clarke E., Grumberg O., Jha S., Lu Y., Veith H. Counterexample-Guided Abstraction Refinement for Symbolic Model Checking // Journal of the ACM. 2003.
27. Thomas Donald, Moorby Phillip. The Verilog Hardware Description Language // Norwell, MA.: Kluwer Academic Publishers.
28. Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs // Tools and Algorithms for the Construction and Analysis of Systems. 2004.
29. Ivancic F., Yang Z., Ganai M.K., Gupta A., I. Shlyakhter, Ashar P. F-soft: Software verification platform // Computer Aided Verification. vol. 3576 of Lecture Notes in Computer Science. Springer, 2005. pp. 301—306.
30. Post H., Sinz C., Merz F., Gorges T., Kropf T. Linking functional requirements and software verification // 17th IEEE International Requirements Engineering Conferene. 2009. pp. 295—302.
31. Donaldson A. F., Kroening D., Ruemmer P. Automatic analysis of DMA races using model checking and k-induction // Formal Methods in System Design. 2011. vol. 39. pp. 83—113.
32. Ball T., Bounimova E., Levin V., Kumar R., Lichtenberg J. The Static Driver Verifier Research Platform // Computer Aided Verification. 2010.
33. D. Beyer, T. A. Henzinger, R. Jhala, R. Majumdar. The software model checker BLAST: Applications to software engineering // Int. J. Softw. Tools Technol. Transf., 2007. vol. 9, № 5, ISSN 1433-2779. Springer-Verlag, Berlin, Heidelberg. pp. 505—525.
34. E. Clarke, D. Kroening, N. Sharygina, K. Yorav. SATABS: SAT-based Predicate Abstraction for ANSI-C // Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), 2005. Lecture Notes in Computer Science, Springer Verlag. vol. 3440. ISBN 3-540-25333-5. pp.570—574.
35. D. Beyer, M. E. Keremoglu. CPAchecker: a tool for configurable software verification // Proceedings of the 23rd international conference on Computer aided verification. 2011. ISBN 978-3-642-22109-5. Springer-Verlag. pp. 184—190.
36. В.С. Мутилин, Е.М. Новиков, А.В. Страх, А.В. Хорошилов, П.Е. Швед. Архитектура Linux Driver Verification. // Труды Института системного программирования РАН, том 20, cтр. 163—187, 2011.
37. A. Khoroshilov, V. Mutilin, E. Novikov, P. Shved, A. Strakh. Towards an Open Framework for C Verification Tools Benchmarking // Proceedings of the Eighth International Andrei Ershov Memorial Conference “Perspectives of Systems Informatics” (PSI 2011), pp. 82—91, 2011.
38. S. Graf, H. Saïdi. Construction of Abstract State Graphs with PVS // Computer Aided Verification, 9th International Conference, CAV '97, Haifa, Israel. pp. 72—83.
39. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G. Lazy abstraction // Proc. POPL. ACM, New York. pp. 58—70, 2002.
40. 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 Trans. Program. Languages Systems 13(4), pp. 451—490. 1991.
41. W. Craig. Linear reasoning // J. Symbolic Logic. 1957. vol. 22, pp. 250—268.
42. Т. A. Henzinger, K. L. McMillan, R. Jhala, R. Majumdar. Abstractions from Proofs. // POPL 2004.
43. D. Beyer, A. Cimatti, A. Griggio, M.E. Keremoglu, R. Sebastiani. Software Model Checking via Large-Block Encoding // Proc. FMCAD, pp. 25—32. IEEE, 2009.
44. D. Beyer, M. E. Keremoglu, P. Wendler. Predicate abstraction with adjustable-block encoding // Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design. Lugano, Switzerland. 2010. pp. 189—198.
45. M. Berndl, O. Lhotak, F. Qian, L. Hendren, N. Umanee. Points-to analysis using BDDs // Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation (PLDI '03). ISBN 1-58113-662-5. San Diego, California, USA. pp.103—114.
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. of Conference on Compiler Construction, 2002, pp. 213—228.
47. Aditya V. Nori and Sriram K. Rajamani. An Empirical Study of Optimizations in Yogi // ICSE '10: International Conference on Software Engineering, May 2010.
48. Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani. The MathSAT5 SMT Solver. // Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, volume 7795, 2013, pp. 93—107.
49. Robert Nieuwenhuis, Alberto Rubio. Paramodulation-Based Theorem Proving // Handbook of Automated Reasoning I (7), Elsevier Science and MIT Press, 2001.
50. D. Kroening, O. Strichman. Decision Procedures. An Algorithmic Point of View // Springer, 2008.
51. M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, S. Ranise, P. van Rossum, R.Sebastiani. Efficient Satisfiability Modulo Theories via Delayed Theory Combination // CAV'05.
52. G. Yorsh, M. Musuvathi. A Combination Method for Generating Interpolants // CADE 2005.
53. A.Rybalchenko, V.Sofronie-Stokkermans. Constraint Solving for Interpolation // AVACS TR No.56, 2009.
54. K. L. McMillan. An Interpolating Theorem Prover // TCS'05.
55. D.Beyer, D.Zufferey, R.Majumdar. CSIsat: Interpolation for LA+EUF. Tool paper. 2008.
56. A.Cimatti, A.Griggio, R.Sebastiani. Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories // ACM Transactions on Computational Logic. vol. 12, issue 1, October 2010.
57. Thi Thieu Hoa Le. A Novel Technique for Computing Craig Interpolants in Satisfiabilility modulo the Theory of Integer Linear Arithmetic. PhD thesis.
58. Leonardo De Moura, Nikolaj Bjørner. Z3: an efficient SMT solver // TACAS'08/ETAPS'08. Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems. pp. 337—340.
59. T. Ball, E. Bounimova, R. Kumar, V. Levin. SLAM2: Static driver verification with under 4% false alarms // Formal Methods in Computer-Aided Design (FMCAD), oct. 2010. pp. 35—42.
60. D. Beyer. Competition on Software Verification // C. Flanagan, B. König eds. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 7214. ISBN 978-3-642-28755-8. Springer Berlin Heidelberg, 2012. pp. 504—524.
61. D. Beyer. Second Competition on Software Verification // N. Piterman, S. A. Smolka eds. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 7795. ISBN 978-3-642-36741-0. Springer Berlin Heidelberg, 2013. pp. 594-609.
62. A. Cimatti, A. Micheli, I. Narasamdya, M. Roveri. Verifying SystemC: A Software Model Checking Approach. // in Proc. FMCAD, FMCAD Inc. 2010. pp. 51–59.
63. A. Galloway, G. Lüttgen, J. T. Mühlberg, R. I. Siminiceanu. Model-Checking the Linux Virtual File System // N. D. Jones, M. Müller-Olm (eds.). VMCAI 2009. LNCS, vol. 5403, pp. 74—88. Springer, Heidelberg. 2009.
64. J. T. Mühlberg, G. Lüttgen. Blasting Linux Code // L. Brim, B. R. Haverkort, M. Leucker, J. van de Pol (eds.). FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 211—226. Springer, Heidelberg (2007)
65. W. Penninckx, J. T. Mühlberg, J. Smans, B. Jacobs, F. Piessens. Sound Formal Verification of Linux’s USB BP Keyboard Driver // A. E. Goodloe, S. Person (eds.). NFM 2012. LNCS, vol. 7226, pp. 210—215. Springer, Heidelberg. 2012.
66. S. Apel, H. Speidel, P. Wendler, A. von Rhein, D. Beyer. Detection of feature interactions using feature-aware verification // 26th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2011, pp.372—375. 6-10 Nov. 2011.
67. A. Classen, P. Heymans, P.-Y. Schobbens, A. Legay. Symbolic model checking of software product lines // in Proceedings of the International Conference on Software Engineering (ICSE). ACM, 2011, pp. 321—330.
68. D. Beyer, T. A. Henzinger, G. Theoduloz. Program Analysis with Dynamic Precision Adjustment // Proc. ASE, pp. 29—38. IEEE (2008)
69. P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, X. Rival. Combination of Abstractions in the ASTREE Static Analyzer // M. Okada, I. Satoh (eds.). ASIAN 2006. LNCS, vol. 4435, pp. 272—300. Springer, Heidelberg (2008)
70. J. Corbet, A. Rubini, G. Kroah-Hartman. Linux Device Drivers, 3rd Edition, Chapter 3, section “The open Method”, pp. 58—59 // O'Reilly Media. 2005.
Рецензия
Для цитирования:
Мандрыкин М.У., Мутилин В.С., Хорошилов А.В. Введение в метод CEGAR - уточнение абстракции по контрпримерам. Труды Института системного программирования РАН. 2013;24.
For citation:
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.)
Послать статью по эл. почте 