ABSTRACT
Program invariants can help software developers identify program properties that must be preserved as the software evolves, however, formulating correct invariants can be challenging. In this work, we introduce iDiscovery, a technique which leverages symbolic execution to improve the quality of dynamically discovered invariants computed by Daikon. Candidate invariants generated by Daikon are synthesized into assertions and instrumented onto the program. The instrumented code is executed symbolically to generate new test cases that are fed back to Daikon to help further refine the set of candidate invariants. This feedback loop is executed until a fix-point is reached. To mitigate the cost of symbolic execution, we present optimizations to prune the symbolic state space and to reduce the complexity of the generated path conditions. We also leverage recent advances in constraint solution reuse techniques to avoid computing results for the same constraints across iterations. Experimental results show that iDiscovery converges to a set of higher quality invariants compared to the initial set of candidate invariants in a small number of iterations.
- A. Baliga, V. Ganapathy, and L. Iftode. Automatic inference and enforcement of kernel data structure invariants. In ACSAC, pages 77–86, 2008. Google ScholarDigital Library
- N. Bjørner, A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. Theor. Comput. Sci., 173(1):49–87, Feb. 1997. Google ScholarDigital Library
- V. Braberman, F. Fernández, D. Garbervetsky, and S. Yovine. Parametric prediction of heap memory requirements. In ISMM, pages 141–150, 2008. Google ScholarDigital Library
- C. Cadar, D. Dunbar, and D. R. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, volume 8, pages 209–224, 2008. Google ScholarDigital Library
- B.-Y. E. Chang and K. R. M. Leino. Abstract interpretation with alien expressions and heap structures. In VMCAI, pages 147–163, 2005. Google ScholarDigital Library
- L. A. Clarke. A program testing system. In Proceedings of the 1976 annual conference, ACM ’76, pages 488–491, 1976. Google ScholarDigital Library
- P. Corporation. Jtest manuals version 4.5 october 23 (2002). http://www.parasoft.com/, 2002.Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238–252, 1977. Google ScholarDigital Library
- C. Csallner, N. Tillmann, and Y. Smaragdakis. DySy: Dynamic symbolic execution for invariant inference. In ICSE, pages 281–290, 2008. Google ScholarDigital Library
- D. D. Dunlop and V. R. Basili. A heuristic for deriving loop functions. IEEE Trans. Softw. Eng., 10(3):275–285, May 1984. Google ScholarDigital Library
- M. D. Ernst. Dynamically discovering likely program invariants. PhD thesis, University of Washington, 2000. Google ScholarDigital Library
- M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program., 69(1-3):35–45, 2007. Google ScholarDigital Library
- C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for ESC/Java. In FME, pages 500–517, 2001. Google ScholarDigital Library
- C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In PLDI, pages 234–245, 2002. Google ScholarDigital Library
- S. M. German and B. Wegbreit. A synthesizer of inductive assertions. In AFIPS, pages 369–376, 1975. Google ScholarDigital Library
- S. Hangal and M. S. Lam. Tracking down software bugs using automatic anomaly detection. In ICSE, pages 291–301, 2002. Google ScholarDigital Library
- F. Howar, D. Giannakopoulou, and Z. Rakamari´ c. Hybrid learning: Interface generation through static, dynamic, and symbolic analysis. In ISSTA, pages 268–279, 2013. Google ScholarDigital Library
- S. Katz and Z. Manna. Logical analysis of programs. Commun. ACM, 19(4):188–206, Apr. 1976. Google ScholarDigital Library
- J. C. King. Symbolic execution and program testing. CACM, 19(7):385–394, 1976. Google ScholarDigital Library
- G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok. How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program., 55(1-3):185–208, Mar. 2005. Google ScholarDigital Library
- K. Li, C. Reichenbach, Y. Smaragdakis, and M. Young. Second-order constraints in dynamic invariant inference. In ESEC/FSE 2013, pages 103–113, 2013. Google ScholarDigital Library
- F. Logozzo. Automatic inference of class invariants. In VMCAI, pages 211–222, 2004.Google ScholarCross Ref
- M. Z. Malik, A. Pervaiz, and S. Khurshid. Generating representation invariants of structurally complex data. In TACAS, pages 34–49, 2007. Google ScholarDigital Library
- B. Meyer, J.-M. Nerson, and M. Matsuo. Eiffel: Object-oriented design for software engineering. In ESEC, pages 221–229, 1987. Google ScholarDigital Library
- J. W. Nimmer and M. D. Ernst. Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java. In RV, 2001.Google Scholar
- C. S. Păsăreanu and N. Rungta. Symbolic Pathfinder: symbolic execution of Java bytecode. In ASE, pages 179–180, 2010. Google ScholarDigital Library
- C. S. Pasareanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In SPIN, pages 164–181, 2004.Google ScholarCross Ref
- N. Polikarpova, I. Ciupa, and B. Meyer. A comparative study of programmer-written and automatically inferred contracts. In ISSTA, pages 93–104, 2009. Google ScholarDigital Library
- SAE-ARP4761. Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment. SAE International, December 1996.Google Scholar
- SIR. Software-artifact infrastructure repository: Home. http://sir.unl.edu, 2008.Google Scholar
- M. Staats, S. Hong, M. Kim, and G. Rothermel. Understanding user understanding: Determining correctness of generated program invariants. In ISSTA, pages 188–198, 2012. Google ScholarDigital Library
- N. Tillmann, F. Chen, and W. Schulte. Discovering likely method specifications. In ICFEM, pages 717–736, 2006. Google ScholarDigital Library
- W. Visser, J. Geldenhuys, and M. B. Dwyer. Green: reducing, reusing and recycling constraints in program analysis. In FSE, page 58, 2012. Google ScholarDigital Library
- B. Wegbreit. The synthesis of loop predicates. Commun. ACM, 17(2):102–113, Feb. 1974. Google ScholarDigital Library
- T. Xie and D. Notkin. Mutually enhancing test generation and specification inference. In In Proc. 3rd International Workshop on Formal Approaches to Testing of Software, pages 60–69, 2003.Google Scholar
- G. Yang, S. Khurshid, S. Person, and N. Rungta. Property differencing for incremental checking. http://cs.txstate.edu/~g_y10/publications/ icse14-iproperty.pdf, to appear in ICSE 2014. Google ScholarDigital Library
- G. Yang, C. S. Păsăreanu, and S. Khurshid. Memoized symbolic execution. In ISSTA, pages 144–154, 2012. Google ScholarDigital Library
Index Terms
Feedback-driven dynamic invariant discovery
Recommendations
Property-directed incremental invariant generation
AbstractA fundamental method of analyzing a system such as a program or a circuit is invariance analysis, in which one proves that an assertion holds on all reachable states. Typically, the proof is performed via induction; however, an assertion, while ...
Inductive invariant generation via abductive inference
OOPSLA '13This paper presents a new method for generating inductive loop invariants that are expressible as boolean combinations of linear integer constraints. The key idea underlying our technique is to perform a backtracking search that combines Hoare-style ...
Invariant functions and invariant relations: An alternative to invariant assertions
Whereas the analysis of loops in imperative programs is, justifiably, dominated by the concept of invariant assertion, we submit a related but different concept, of invariant relation, and show how it can be used to analyze diverse aspects of a while ...
Comments