Feedback-driven dynamic invariant discovery

Lingming Zhang, Guowei Yang, Neha Rungta, Suzette Person, Sarfraz Khurshid

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 I Discovery converges to a set of higher quality invariants compared to the initial set of candidate invariants in a small number of iterations.

Original languageEnglish (US)
Title of host publication2014 International Symposium on Software Testing and Analysis, ISSTA 2014 - Proceedings
PublisherAssociation for Computing Machinery, Inc
Pages362-372
Number of pages11
ISBN (Electronic)9781450326452
DOIs
StatePublished - Jul 21 2014
Externally publishedYes
Event23rd International Symposium on Software Testing and Analysis, ISSTA 2014 - San Jose, United States
Duration: Jul 21 2014Jul 25 2014

Publication series

Name2014 International Symposium on Software Testing and Analysis, ISSTA 2014 - Proceedings

Other

Other23rd International Symposium on Software Testing and Analysis, ISSTA 2014
Country/TerritoryUnited States
CitySan Jose
Period7/21/147/25/14

Keywords

  • Invariant generation
  • Model checking
  • Symbolic execution

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Feedback-driven dynamic invariant discovery'. Together they form a unique fingerprint.

Cite this