DySy: dynamic symbolic execution for invariant inference

ABSTRACT

Dynamically discovering likely program invariants from concrete test executions has emerged as a highly promising software engineering technique. Dynamic invariant inference has the advantage of succinctly summarizing both "expected" program inputs and the subset of program behaviors that is normal under those inputs. In this paper, we introduce a technique that can drastically increase the relevance of inferred invariants, or reduce the size of the test suite required to obtain good invariants. Instead of falsifying invariants produced by pre-set patterns, we determine likely program invariants by combining the concrete execution of actual test cases with a simultaneous symbolic execution of the same tests. The symbolic execution produces abstract conditions over program variables that the concrete tests satisfy during their execution. In this way, we obtain the benefits of dynamic inference tools like Daikon: the inferred invariants correspond to the observed program behaviors. At the same time, however, our inferred invariants are much more suited to the program at hand than Daikon's hard-coded invariant patterns. The symbolic invariants are literally derived from the program text itself, with appropriate value substitutions as dictated by symbolic execution.

We implemented our technique in the DySy tool, which utilizes a powerful symbolic execution and simplification engine. The results confirm the benefits of our approach. In Daikon's prime example benchmark, we infer the majority of the interesting Daikon invariants, while eliminating invariants that a human user is likely to consider irrelevant.

REFERENCES

• 1: Glenn Ammons , Rastislav Bodík , James R. Larus, Mining specifications, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.4-16, January 16-18, 2002, Portland, Oregon
• 2: Marat Boshernitsan , Roongko Doong , Alberto Savoia, From daikon to agitator: lessons and challenges in building a commercial tool for developer testing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146258]
• 3: Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
• 4: M. Colón, S. Sankaranarayanan, and H. Sipma. Linear invariant generation using non-linear constraint solving. In Proc. 15th International Conference on Computer-Aided Verification (CAV), pages 420--432. Springer, July 2003.
• 5: Christoph Csallner , Yannis Smaragdakis, DSD-Crasher: a hybrid analysis tool for bug finding, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146267]
• 6: Christoph Csallner , Yannis Smaragdakis, Dynamically discovering likely interface invariants, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134435]
• 7: Christoph Csallner , Yannis Smaragdakis, Dynamically discovering likely interface invariants, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134435]
• 8: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically discovering likely program invariants to support program evolution, Proceedings of the 21st international conference on Software engineering, p.213-224, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302467]
• 9: 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]
• 10: Michael D. Ernst , Jeff H. Perkins , Philip J. Guo , Stephen McCamant , Carlos Pacheco , Matthew S. Tschantz , Chen Xiao, The Daikon system for dynamic detection of likely invariants, Science of Computer Programming, v.69 n.1-3, p.35-45, December, 2007 [doi>10.1016/j.scico.2007.01.015]
• 11: David Evans , Michael Peck, Inculcating invariants in introductory courses, Proceedings of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134388]
• 12: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 13: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 14: Cormac Flanagan , Shaz Qadeer, Predicate abstraction for software verification, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-202, January 16-18, 2002, Portland, Oregon
• 15: G. C. Gannod , B. H. C. Cheng, Strongest postcondition semantics as the formal basis for reverse engineering, Proceedings of the Second Working Conference on Reverse Engineering, p.188, July 14-16, 1995
• 16: Gerald C. Gannod , Betty H. C. Cheng, A specification matching based approach to reverse engineering, Proceedings of the 21st international conference on Software engineering, p.389-398, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302661]
• 17: 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
• 18: Sudheendra Hangal , Monica S. Lam, Tracking down software bugs using automatic anomaly detection, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581377]
• 19: J. Henkel and A. Diwan. Discovering algebraic specifications from Java classes. In Proc. 17th European Conference on Object-Oriented Programming (ECOOP), pages 431--456. Springer, July 2003.
• 20: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 21: A. K. Kolawa. Method and system for generating a computer program test suite using dynamic symbolic execution of Java programs. United States Patent 5784553, July 1998.
• 22: Nadya Kuzmina , Ruben Gamboa, Extending Dynamic Constraint Detection with Polymorphic Analysis, Proceedings of the 5th International Workshop on Dynamic Analysis, p.1, May 20-26, 2007 [doi>10.1109/WODA.2007.3]
• 23: G. T. Leavens, A. L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR98-06y, Department of Computer Science, Iowa State University, June 1998.
• 24: Zhenmin Li , Yuanyuan Zhou, PR-Miner: automatically extracting implicit programming rules and detecting violations in large software code, 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
• 25: Ben Liblit , Mayur Naik , Alice X. Zheng , Alex Aiken , Michael I. Jordan, Scalable statistical bug isolation, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 26: F. Logozzo. Modular Static Analysis of Object-Oriented Languages. PhD thesis, Ecole Polytechnique, June 2004.
• 27: 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]
• 28: C. S. Pasareanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In Proc. 11th International SPIN Workshop, pages 164--181. Springer, Apr. 2004.
• 29: Jeff H. Perkins , Michael D. Ernst, Efficient incremental algorithms for dynamic detection of likely invariants, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 30: 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
• 31: Mana Taghdiri, Inferring Specifications to Detect Errors in Code, Proceedings of the 19th IEEE international conference on Automated software engineering, p.144-153, September 20-24, 2004 [doi>10.1109/ASE.2004.42]
• 32: N. Tillmann, F. Chen, and W. Schulte. Discovering likely method specifications. In Proc. 8th International Conference on Formal Engineering Methods (ICFEM'06), LNCS. Springer-Verlag, 2006.
• 33: N. Tillmann and J. de Halleux. Pex - white box test generation for .NET. In Proc. Second International Conference on Tests and Proofs (TAP). Springer, Apr. 2008. To appear.
• 34: Mark Allen Weiss, Data Structures and Algorithm Analysis in Java, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1998
• 35: John Whaley , Michael C. Martin , Monica S. Lam, Automatic extraction of object-oriented component interfaces, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 36: Tao Xie , David Notkin, Tool-assisted unit-test generation and selection based on operational abstractions, Automated Software Engineering, v.13 n.3, p.345-371, July 2006 [doi>10.1007/s10851-006-8530-6]
• 37: Jinlin Yang , David Evans, Dynamically inferring temporal properties, Proceedings of the 5th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, June 07-08, 2004, Washington DC, USA [doi>10.1145/996821.996832]

INDEX TERMS

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

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

General Terms:
Design, Languages

Keywords:
daikon, dynamic invariant inference, dysy, pex, symbolic reasoning