skip to main content
10.1145/2610384.2610389acmconferencesArticle/Chapter ViewAbstractPublication PagesisstaConference Proceedingsconference-collections
research-article

Feedback-driven dynamic invariant discovery

Published:21 July 2014Publication History

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.

References

  1. A. Baliga, V. Ganapathy, and L. Iftode. Automatic inference and enforcement of kernel data structure invariants. In ACSAC, pages 77–86, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  3. V. Braberman, F. Fernández, D. Garbervetsky, and S. Yovine. Parametric prediction of heap memory requirements. In ISMM, pages 141–150, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  5. B.-Y. E. Chang and K. R. M. Leino. Abstract interpretation with alien expressions and heap structures. In VMCAI, pages 147–163, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. L. A. Clarke. A program testing system. In Proceedings of the 1976 annual conference, ACM ’76, pages 488–491, 1976. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. P. Corporation. Jtest manuals version 4.5 october 23 (2002). http://www.parasoft.com/, 2002.Google ScholarGoogle Scholar
  8. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  9. C. Csallner, N. Tillmann, and Y. Smaragdakis. DySy: Dynamic symbolic execution for invariant inference. In ICSE, pages 281–290, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. D. D. Dunlop and V. R. Basili. A heuristic for deriving loop functions. IEEE Trans. Softw. Eng., 10(3):275–285, May 1984. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. M. D. Ernst. Dynamically discovering likely program invariants. PhD thesis, University of Washington, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  13. C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for ESC/Java. In FME, pages 500–517, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  15. S. M. German and B. Wegbreit. A synthesizer of inductive assertions. In AFIPS, pages 369–376, 1975. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. S. Hangal and M. S. Lam. Tracking down software bugs using automatic anomaly detection. In ICSE, pages 291–301, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  18. S. Katz and Z. Manna. Logical analysis of programs. Commun. ACM, 19(4):188–206, Apr. 1976. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. J. C. King. Symbolic execution and program testing. CACM, 19(7):385–394, 1976. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  21. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  22. F. Logozzo. Automatic inference of class invariants. In VMCAI, pages 211–222, 2004.Google ScholarGoogle ScholarCross RefCross Ref
  23. M. Z. Malik, A. Pervaiz, and S. Khurshid. Generating representation invariants of structurally complex data. In TACAS, pages 34–49, 2007. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. B. Meyer, J.-M. Nerson, and M. Matsuo. Eiffel: Object-oriented design for software engineering. In ESEC, pages 221–229, 1987. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. J. W. Nimmer and M. D. Ernst. Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java. In RV, 2001.Google ScholarGoogle Scholar
  26. C. S. Păsăreanu and N. Rungta. Symbolic Pathfinder: symbolic execution of Java bytecode. In ASE, pages 179–180, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. C. S. Pasareanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In SPIN, pages 164–181, 2004.Google ScholarGoogle ScholarCross RefCross Ref
  28. N. Polikarpova, I. Ciupa, and B. Meyer. A comparative study of programmer-written and automatically inferred contracts. In ISSTA, pages 93–104, 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. SAE-ARP4761. Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment. SAE International, December 1996.Google ScholarGoogle Scholar
  30. SIR. Software-artifact infrastructure repository: Home. http://sir.unl.edu, 2008.Google ScholarGoogle Scholar
  31. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  32. N. Tillmann, F. Chen, and W. Schulte. Discovering likely method specifications. In ICFEM, pages 717–736, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. W. Visser, J. Geldenhuys, and M. B. Dwyer. Green: reducing, reusing and recycling constraints in program analysis. In FSE, page 58, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  34. B. Wegbreit. The synthesis of loop predicates. Commun. ACM, 17(2):102–113, Feb. 1974. Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. 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 ScholarGoogle Scholar
  36. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  37. G. Yang, C. S. Păsăreanu, and S. Khurshid. Memoized symbolic execution. In ISSTA, pages 144–154, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Feedback-driven dynamic invariant discovery

              Recommendations

              Comments

              Login options

              Check if you have access through your login credentials or your institution to get full access on this article.

              Sign in
              • Published in

                cover image ACM Conferences
                ISSTA 2014: Proceedings of the 2014 International Symposium on Software Testing and Analysis
                July 2014
                460 pages
                ISBN:9781450326452
                DOI:10.1145/2610384

                Copyright © 2014 ACM

                Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

                Publisher

                Association for Computing Machinery

                New York, NY, United States

                Publication History

                • Published: 21 July 2014

                Permissions

                Request permissions about this article.

                Request Permissions

                Check for updates

                Qualifiers

                • research-article

                Acceptance Rates

                Overall Acceptance Rate58of213submissions,27%

              PDF Format

              View or Download as a PDF file.

              PDF

              eReader

              View online with eReader.

              eReader