Testing, abstraction, theorem proving: better together!

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.

REFERENCES

• 1: T. Ball. A theory of predicate-complete test coverage and generation. In 3rd International Symposium on Formal Methods for Components and Objects, 2004.
• 2: 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
• 3: 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.
• 4: K. Claessen and N. Sorensson. New techniques that improve mace-style finite model finding. In CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications, 2003.
• 5: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 6: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 7: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 8: Christoph Csallner , Yannis Smaragdakis, Check 'n' crash: combining static checking and testing, Proceedings of the 27th international conference on Software engineering, p.422-431, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062533]
• 9: D. Dams. Abstract Interpretation and Partial Refinement for Model Checking. PhD thesis, Technical Univ. of Eindhoven, Eindhoven, The Netherlands, July 1996.
• 10: 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.
• 11: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 12: G. Erez. Generating concrete counter examples for arbitrary abstract domains. Master's thesis, Tel-Aviv University, Israel, 2004.
• 13: 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.
• 14: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 15: 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.
• 16: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 17: 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
• 18: W. Grieskamp, N. Tillmann, and W. Schulte. Xrt exploring runtime for .net: Architecture and applications. In SoftMC, 2005.
• 19: Mary Jean Harrold, Testing: a roadmap, Proceedings of the Conference on The Future of Software Engineering, p.61-72, June 04-11, 2000, Limerick, Ireland [doi>10.1145/336512.336532]
• 20: T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with blast. In SPIN, pages 235--239, 2003.
• 21: G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.
• 22: David Lee , Mihalis Yannakakis, Online minimization of transition systems (extended abstract), Proceedings of the twenty-fourth annual ACM symposium on Theory of computing, p.264-274, May 04-06, 1992, Victoria, British Columbia, Canada [doi>10.1145/129712.129738]
• 23: K. R. M. Leino, G. Nelson, and J. B. Saxe. Esc/java users manual. Technical Report 002, Compaq Systems Research Center, 2000.
• 24: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 25: F. Logozzo. Modular Static Analysis of Object Oriented Languages. PhD thesis, LEcole Polytechnique, 2004.
• 26: Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, Proceedings of the 5th symposium on Operating systems design and implementation

  Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading

  , December 09-11, 2002, Boston, Massachusetts [doi>10.1145/1060289.1060297]
• 27: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 28: Jeremy W. Nimmer , Michael D. Ernst, Invariant inference for static checking:, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587054]
• 29: C. Pasareanu, R. Pelanek, and W. Visser. Concrete model checking with abstract matching and refinement. In CAV, 2005.
• 30: Alexandre Riazanov , Andrei Voronkov, Vampire 1.1 (System Description), Proceedings of the First International Joint Conference on Automated Reasoning, p.376-380, June 18-23, 2001
• 31: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 32: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 33: T.Reps, M. Sagiv, and G. Yorsh. Symbolic implementation of the best transformer. In VMCAI, pages 252--266, 2004.
• 34: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 35: C. Weidenbach. SPASS: An automated theorem prover for first-order logic with equality. Available at "http://spass.mpi-sb.mpg.de/index.html".
• 36: G. Yorsh, T. Reps, and M. Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In TACAS, 2004.
• 37: Hong Zhu , Patrick A. V. Hall , John H. R. May, Software unit test coverage and adequacy, ACM Computing Surveys (CSUR), v.29 n.4, p.366-427, Dec. 1997 [doi>10.1145/267580.267590]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Reliability, Verification

Keywords:
abstract interpretation, abstraction, adequacy criteria, coverage, fabricated states, program analysis, software fault injection, state-based coverage, testing, theorem prover