Greta Yorsh
ABSTRACT
We present a method for static program analysis that leverages tests and concrete program executions. State abstractions generalize the set of program states obtained from concrete executions. A theorem prover then checks that the generalized set of concrete states covers all potential executions and satisfies additional safety properties. Our method finds the same potential errors as the mostprecise abstract interpreter for a given abstraction and is potentially more efficient. Additionally, it provides a new way to tune the performance of the analysis by alternating between concrete execution and theorem proving. We have implemented our technique in a prototype for checking properties of C# programs.
- T. Ball. A theory of predicate-complete test coverage and generation. In 3rd International Symposium on Formal Methods for Components and Objects, 2004. Google Scholar
Digital Library
- T. Ball, R. Majumdar, T. D. Millstein, and S. K. Rajamani. Automatic predicate abstraction of c programs. In SIGPLAN Conf. on Prog. Lang. Design and Impl., pages 203--213, 2001. Google ScholarDigital Library
- P. Baumgartner, A. Fuchs, and C. Tinelli. Implementing the Model Evolution Calculus. In Stephan Schulz, Geoff Sutcliffe, and Tanel Tammet, editors, Special Issue of the International Journal of Artificial Intelligence Tools (IJAIT), International Journal of Artificial Intelligence Tools, 2005. Preprint.Google Scholar
- K. Claessen and N. Sorensson. New techniques that improve mace-style finite model finding. In CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications, 2003.Google Scholar
- E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. Trans. on Prog. Lang. and Syst., 16(5):1512--1542, 1994. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Symp. on Princ. of Prog. Lang., pages 238--252, New York, NY, 1977. ACM Press. Google ScholarDigital Library
- P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Symp. on Princ. of Prog. Lang., pages 84--96, 1978. Google ScholarDigital Library
- C. Csallner and Y. Smaragdakis. Check 'n' crash: combining static checking and testing. In ICSE, pages 422--431, 2005. Google ScholarDigital Library
- D. Dams. Abstract Interpretation and Partial Refinement for Model Checking. PhD thesis, Technical Univ. of Eindhoven, Eindhoven, The Netherlands, July 1996.Google Scholar
- D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs, 2003. http://research.compaq.com/SRC/esc/Simplify.html.Google Scholar
- E.W. Dijksta. A Discipline of Programming. Prentice-Hall, 1976. Google ScholarDigital Library
- G. Erez. Generating concrete counter examples for arbitrary abstract domains. Master's thesis, Tel-Aviv University, Israel, 2004.Google Scholar
- M. D. Ernst. Static and dynamic analysis: Synergy and duality. In WODA 2003: ICSE Workshop on Dynamic Analysis, pages 24--27, Portland, OR, May 9, 2003. Google ScholarDigital Library
- M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE TSE, 27(2):1--25, February 2001. Google ScholarDigital Library
- R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics 19, pages 19--32, Providence, 1967. American Mathematical Society.Google Scholar
- P. Godefroid, N. Klarlund, and K. Sen. Dart: directed automated random testing. In SIGPLAN Conf. on Prog. Lang. Design and Impl., pages 213--223, 2005. Google ScholarDigital Library
- S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In CAV, pages 72--83, June 1997. Google ScholarDigital Library
- W. Grieskamp, N. Tillmann, and W. Schulte. Xrt exploring runtime for .net: Architecture and applications. In SoftMC, 2005.Google Scholar
- M. J. Harrold. Testing: a roadmap. In ICSE - Future of SE Track, pages 61--72, 2000. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with blast. In SPIN, pages 235--239, 2003. Google ScholarDigital Library
- G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2003. Google ScholarDigital Library
- D. Lee and M. Yannakakis. Online minimization of transition systems (extended abstract). In STOC, pages 264--274, 1992. Google ScholarDigital Library
- K. R. M. Leino, G. Nelson, and J. B. Saxe. Esc/java users manual. Technical Report 002, Compaq Systems Research Center, 2000.Google Scholar
- T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In Static Analysis Symp., pages 280--301, 2000. The system is available from www.cs.tau.ac.il/~tvla. Google ScholarDigital Library
- F. Logozzo. Modular Static Analysis of Object Oriented Languages. PhD thesis, LEcole Polytechnique, 2004.Google Scholar
- M. Musuvathi, D. Y. W. Park, A. Chou, D. R. Engler, and D. L. Dill. Cmc: A pragmatic approach to model checking real code. In OSDI, 2002. Google ScholarDigital Library
- F. Nielson, H.R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999. Google ScholarDigital Library
- J. W. Nimmer and M. D. Ernst. Invariant inference for static checking: An empirical evaluation. In FSE 2002, pages 11--20, 2002. Google ScholarDigital Library
- C. Pasareanu, R. Pelanek, and W. Visser. Concrete model checking with abstract matching and refinement. In CAV, 2005. Google ScholarDigital Library
- A. Riazanov and A. Voronkov. Vampire 1.1 (system description). In IJCAR, pages 376--380, 2001. Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst., 2002. Google ScholarDigital Library
- K. Sen, D. Marinov, and G. Agha. Cute: a concolic unit testing engine for c. In ESEC/SIGSOFT FSE, pages 263--272, 2005. Google ScholarDigital Library
- T.Reps, M. Sagiv, and G. Yorsh. Symbolic implementation of the best transformer. In VMCAI, pages 252--266, 2004.Google ScholarCross Ref
- W. Visser, K. Havelund, G. P. Brat, S. Park, and F. Lerda. Model checking programs. Autom. Softw. Eng., 10(2):203--232, 2003. Google ScholarDigital Library
- C. Weidenbach. SPASS: An automated theorem prover for first-order logic with equality. Available at "http://spass.mpi-sb.mpg.de/index.html".Google Scholar
- G. Yorsh, T. Reps, and M. Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In TACAS, 2004.Google ScholarCross Ref
- H. Zhu, P.A. Hall, and H.R. May. Software unit test coverage and adequacy. ACM Computing Surveys, 29(4):336--427, December 1997. Google ScholarDigital Library
Index Terms
- Testing, abstraction, theorem proving: better together!
Recommendations
Conditional model checking: a technique to pass information between verifiers
FSE '12: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software EngineeringSoftware model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself ...
Theorem proving: not an esoteric diversion, but the unifying framework for industrial verification
ICCD '95: Proceedings of the 1995 International Conference on Computer Design: VLSI in Computers and ProcessorsThe effectiveness of hardware verification techniques has increased markedly in the past decade. As hardware verification techniques become increasingly powerful the idea of transitioning verification technology to industry can be taken seriously. ...
PVS Strategies for Proving Abstraction Properties of Automata
Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct abstraction relation between the states of the automata, ...
Comments