SYNERGY: a new algorithm for property checking

ABSTRACT

We 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 approaches to property checking are testing and verification. Testing tries to find inputs and executions which demonstrate violations of the property. Verification tries to construct a formal proof which shows that all executions of the program satisfy the property. Testing works best when errors are easy to find, but it is often difficult to achieve sufficient coverage for correct programs. On the other hand, verification methods are most successful when proofs are easy to find, but they are often inefficient at discovering errors. We propose a new algorithm, Synergy, which combines testing and verification. Synergy unifies several ideas from the literature, including counterexample-guided model checking, directed testing, and partition refinement.This paper presents a description of the Synergy algorithm, its theoretical properties, a comparison with related algorithms, and a prototype implementation called Yogi.

REFERENCES

• 1: F#:http://research.microsoft.com/fsharp/fsharp.aspx
• 2: T. Ball, S. Lahiri, M. Musuvathi. zap: Automated theorem proving for software analysis. Tech. Rep. MSR-TR-2005-137, Microsoft Research, 2005.
• 3: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 4: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 5: Modular Verification of Software Components in C, IEEE Transactions on Software Engineering, v.30 n.6, p.388-402, June 2004 [doi>10.1109/TSE.2004.22]
• 6: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 7: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 8: 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]
• 9: J. Edvardsson. A survey on automatic test data generation. In Computer Science and Engineering in Linköping, pp. 21--28. ECSEL, 1999.
• 10: D. Engler, B. Chelf, A. Chou, S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Operating System Design and Implementation, pp. 1--16. Usenix, 2000.
• 11: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 12: P. Godefroid and N. Klarlund. Software model checking: Searching for computations in the abstract or the concrete. In Integrated Formal Methods, LNCS 3771, pp. 20--32. Springer, 2005.
• 13: 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
• 14: B.S. Gulavani and S.K. Rajamani. Counterexample- driven refinement for abstract interpretation. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 3920, pp. 474--488. Springer, 2006.
• 15: Elsa Gunter , Doron Peled, Model checking, testing and verification working together, Formal Aspects of Computing, v.17 n.2, p.201-221, August 2005 [doi>10.1007/s00165-005-0059-8]
• 16: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-244, January 14-16, 2004, Venice, Italy
• 17: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 18: Ranjit Jhala , Rupak Majumdar, Path slicing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 19: R. Jhala and K.L. McMillan. A practical and complete approach to predicate refinement. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 3920, pp. 459--473. Springer, 2006.
• 20: Paris C. Kanellakis , Scott A. Smolka, CCS expressions finite state processes, and three problems of equivalence, Information and Computation, v.86 n.1, p.43-68, May 1990 [doi>10.1016/0890-5401(90)90025-D]
• 21: D. Kröning, A. Groce, E.M. Clarke. Counterexample- guided abstraction refinement via program execution. In Formal Engineering Methods (ICFEM), LNCS 3308, pp. 224--238. Springer, 2004.
• 22: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 23: 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]
• 24: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 25: R. Milner. An algebraic definition of simulation between programs. In Artificial Intelligence (IJCAI), pp. 481--489. British Computer Society, 1971.
• 26: Robert Paige , Robert E. Tarjan, Three partition refinement algorithms, SIAM Journal on Computing, v.16 n.6, p.973-989, December 1, 1987 [doi>10.1137/0216062]
• 27: C.S. Pasareanu, R. Pelánek, W. Visser. Concrete model checking with abstract matching and refinement. In Computer-Aided Verification, LNCS 3576, pp. 52--66. Springer, 2005.
• 28: A. Srivastava, A. Edwards, H. Vo. vulcan: Binary transformation in a distributed environment. Tech. Rep. MSR-TR-2001-50, Microsoft Research, 2001.
• 29: Greta Yorsh , Thomas Ball , Mooly Sagiv, Testing, abstraction, theorem proving: better together!, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146255]

INDEX TERMS

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

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

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Verification

Keywords:
abstraction refinement, directed testing, software model checking, testing