Patrice Godefroid
ABSTRACT
Program analysis tools typically compute two types of information: (1) may information that is true of all program executions and is used to prove the absence of bugs in the program, and (2) must information that is true of some program executions and is used to prove the existence of bugs in the program. In this paper, we propose a new algorithm, dubbed SMASH, which computes both may and must information compositionally . At each procedure boundary, may and must information is represented and stored as may and must summaries, respectively. Those summaries are computed in a demand driven manner and possibly using summaries of the opposite type. We have implemented SMASH using predicate abstraction (as in SLAM) for the may part and using dynamic test generation (as in DART) for the must part. Results of experiments with 69 Microsoft Windows 7 device drivers show that SMASH can significantly outperform may-only, must-only and non-compositional may-must algorithms. Indeed, our empirical results indicate that most complex code fragments in large programs are actually often either easy to prove irrelevant to the specific property of interest using may analysis or easy to traverse using directed testing. The fine-grained coupling and alternation of may (universal) and must (existential) summaries allows SMASH to easily navigate through these code fragments while traditional may-only, must-only or non-compositional may-must algorithms are stuck in their specific analyses.
- S. Anand, P. Godefroid, and N. Tillmann. Demand-driven compositional symbolic execution. In TACAS '08: Tools and Algorithms for the Construction and Analysis of Systems, pages 367--381, 2008. Google Scholar
Digital Library
- T. Ball, O. Kupferman, and G. Yorsh. Abstraction for falsification. In CAV '05: Computer-Aided Verification, 2005. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN '00: International SPIN Workshop, pages 113--130, 2000. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN '01: SPIN workshop on Model checking of Software, pages 103--122, 2001. Google ScholarDigital Library
- N. E. Beckman, A. V. Nori, S. K. Rajamani, and R. J. Simmons. Proofs from tests. In ISSTA'08: International Symposium on Software Testing and Analysis, pages 3--14, 2008. Google ScholarDigital Library
- D. Beyer, T. A. Henzinger, and G. Theoduloz. Program analysis with dynamic precision adjustment. In ASE '08: Automated Software Engineering, 2008. Google ScholarDigital Library
- W.R. Bush, J.D. Pincus, and D.J. Sielaff. A static analyzer for finding dynamic programming errors. Software Practice and Experience, 30(7):775--802, 2000. Google ScholarDigital Library
- C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically generating inputs of death. In CCS '06: Computer and Communications Security Conference, 2006. Google ScholarDigital Library
- B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In PLDI '06: Programming Language Design and Implementation, 2006. Google ScholarDigital Library
- C. Csallner and Y. Smaragdakis. Check'n Crash: Combining static checking and testing. In ICSE '05: International Conference on Software Engineering, 2005. Google ScholarDigital Library
- M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In PLDI'02: Programming Language Design and Implementation, pages 57--69, 2002. Google ScholarDigital Library
- L. de Moura and N. Bjorner. Z3: An Efficient SMT Solver. In TACAS '08: Tools and Algorithms for the Construction and Analysis of Systems, 2008. Google ScholarDigital Library
- I. Dillig, T. Dillig, and A. Aiken. Sound, complete and scalable path-sensitive analysis. In PLDI '08: Programming Language Design and Implementation, pages 270--280, 2008. Google ScholarDigital Library
- P. Godefroid. Compositional dynamic test generation. In POPL '07: Principles of Programming Languages, pages 47--54, 2007. Google ScholarDigital Library
- P. Godefroid, M. Huth, and R. Jagadeesan. Abstraction-based model checking using modal transition systems. In CONCUR '01: International Conference on Concurrency Theory, pages 426--440, 2001. Google ScholarDigital Library
- P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In PLDI '05: Programming Language Design and Implementation, pages 213--223, 2005. Google ScholarDigital Library
- P. Godefroid, M.Y. Levin, and D. Molnar. Active property checking. In EMSOFT '08: Annual Conference on Embedded Software, pages 207--216, 2008. Google ScholarDigital Library
- P. Godefroid, M.Y. Levin, and D. Molnar. Automated whitebox fuzz testing. In NDSS '08: Network and Distributed Systems Security, pages 151--166, 2008.Google Scholar
- B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori, and S. K. Rajamani. synergy: A new algorithm for property checking. In FSE '06: Foundations of Software Engineering, pages 117--127, 2006. Google ScholarDigital Library
- A. K. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R-G. Xu. Proving non-termination. In POPL '08: Principles of Programming Languages, pages 147--158, 2008. Google ScholarDigital Library
- A. Gurfinkel, O. Wei, and M. Chechik. Yasm: A software model checker for verification and refutation. In CAV '06: Computer-Aided Verification, pages 170--174, 2006. Google ScholarDigital Library
- A. Gurfinkel, O. Wei, and M. Chechik. Model checking recursive programs with exact predicate abstraction. In ATVA '08: Automated Technology for Verification and Analysis, pages 95--110, 2008. Google ScholarDigital Library
- S. Hallem, B. Chelf, Y. Xie, and D. Engler. A system and language for building system-specific static analyses. In PLDI'02: Programming Language Design and Implementation, pages 69--82, 2002. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL '02: Principles of Programming Languages, pages 58--70, 2002. Google ScholarDigital Library
- S. Horwitz, T. Reps, and M. Sagiv. Demand interprocedural dataflow analysis. In FSE '95: Foundations of Software Engineering, pages 104--115, 1995. Google ScholarDigital Library
- Y. Kesten and A. Pnueli. Verification by augmented finitary abstraction. Information and Computation, 163(1), 2000. Google ScholarDigital Library
- K. L. McMillan. Interpolation and SAT--based model checking. In CAV '03: Computer-Aid Verification, pages 1--13, 2003.Google ScholarCross Ref
- G. C. Necula, S. McPeak, and W. Weimer. CCured: Type-safe retrofitting of legacy code. In POPL '02: Principles of Programming Languages, pages 128--139, 2002. Google ScholarDigital Library
- A. V. Nori, S. K Rajamani, S. Tetali, and A. V. Thakur. The Yogi Project: Software property checking via static analysis and testing. In TACAS '09: Tools and Algorithms for the Construction and Analysis of Systems, pages 178--181, 2009. Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In POPL '99: Principles of Programming Languages, pages 105--118, 1999. Google ScholarDigital Library
- T. Uribe. Abstraction-based Deductive-Algorithmic Verification of Reactive Systems. PhD thesis, Stanford University, 1999. Google ScholarDigital Library
- W. Visser, C. Pasareanu, and S. Khurshid. Test input generation with java pathfinder. In ISSTA '04: International Symposium on Software Testing and Analysis, 2004. Google ScholarDigital Library
Index Terms
- Compositional may-must program analysis: unleashing the power of alternation
Recommendations
Compositional may-must program analysis: unleashing the power of alternation
POPL '10Program analysis tools typically compute two types of information: (1) may information that is true of all program executions and is used to prove the absence of bugs in the program, and (2) must information that is true of some program executions ...
SYNERGY: a new algorithm for property checking
SIGSOFT '06/FSE-14: Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineeringWe consider the problem if a given program satisfies a specified safety property. Interesting programs have infinite state spaces, with inputs ranging over infinite domains, and for these programs the property checking problem is undecidable. Two broad ...
Compositional Abstraction Refinement for Timed Systems
TASE '10: Proceedings of the 2010 4th IEEE International Symposium on Theoretical Aspects of Software EngineeringModel checking suffers from the state explosion problem. Compositional abstraction and abstraction refinement have been investigated in many areas to address this problem. This paper considers the compositional model checking for timed systems. We ...
Reviews
Prahladavaradan Sampath
The problem of software model checking is quite simply stated: is it possible to reach a particular instruction in the program when executing it__?__ This paper is the culmination of nearly a decade of effort toward solving this problem. The commercial driver behind this effort has been to improve the quality of the basic operating system (OS) code that runs on over one billion personal computers (PCs). The early part of this decade saw a breakthrough in software model checking: abstraction refinement techniques were effectively used to solve this problem. This work is based on the use of predicate abstraction to over-approximate a program-a technique that answers the question of unreachability of a program location. The latter part of the decade saw some progress in how advances in test case generation could be used to under-approximate the program and help in refining the predicate abstraction. The essential insight is that the reachability relation induced by test cases is the counterpart to the unreachability relation used by the predicate abstraction approach to software model checking. This paper shows how memoization techniques can be effectively used to make the software model-checking procedure compositional across procedures. Another important contribution-one with pedagogical significance-is the rule-based presentation of the software model-checking procedure. The presentation is very appealing and brings out the essential ideas, without cluttering the paper with the detailed algorithmic considerations that make such a procedure work on real programs. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments