SymInfer: Inferring Program Invariants using Symbolic States. Nguyen, T., Dwyer, M., & Visser, W. In Automated Software Engineering (ASE), pages to appear, 2017. IEEE.
SymInfer: Inferring Program Invariants using Symbolic States [pdf]Paper  SymInfer: Inferring Program Invariants using Symbolic States [pdf]Slides  SymInfer: Inferring Program Invariants using Symbolic States [link]Code  abstract   bibtex   
We introduce a new technique for inferring program invariants that uses symbolic states generated by symbolic execution. Symbolic states, which consist of path conditions and constraints on local variables, are a compact description of sets of concrete program states and they can be used for both invariant inference and invariant verification. Our technique uses a counterexample-based algorithm that creates concrete states from symbolic states, infers candidate invariants from concrete states, and then verifies or refutes candidate invariants using symbolic states. The refutation case produces concrete counterexamples that prevent spurious results and allow the technique to obtain more precise invariants. This process stops when the algorithm reaches a stable set of invariants. We present SymInfer, a tool that implements these ideas to automatically generate invariants at arbitrary locations in a Java program. The tool obtains symbolic states from Symbolic PathFinder and uses existing algorithms to infer complex (potentially nonlinear) numerical invariants. Our preliminary results show that SymInfer is effective in using symbolic states to generate precise and useful invariants for proving program safety and analyzing program runtime complexity. We also show that SymInfer outperforms existing invariant generation systems.
@inproceedings{symtracesase17,
	Author = {Nguyen, ThanhVu and Dwyer, Matthew and Visser, William},
	Booktitle = {Automated Software Engineering (ASE)},
	Publisher = {IEEE},
	Pages = {to appear},
	Bibbase_Note = {},
	Title = {{SymInfer: Inferring Program Invariants using Symbolic States}},
        Url_paper = {Pub/symtraces.pdf},
	Url_slides = {Pub/symtraces_pres.pdf},			
	Url_code = {https://bitbucket.org/nguyenthanhvuh/symtraces/},
	Year = {2017},
	Abstract = {
We introduce a new technique for inferring program invariants that uses symbolic
states generated by symbolic execution.  Symbolic states,
which consist of path conditions and constraints on local variables, 
are a compact description of sets of concrete program states and they
can be used for both invariant inference and invariant verification. 
Our technique uses a
counterexample-based algorithm that creates
concrete states from symbolic states, infers candidate
invariants from concrete states, and then verifies or refutes candidate
invariants using symbolic states.  The refutation case produces concrete
counterexamples that prevent spurious results and allow the technique to
obtain more precise invariants.  This process stops when the algorithm reaches
a stable set of invariants.

We present SymInfer, a tool that implements these ideas to automatically
generate invariants at arbitrary locations in a Java program.  The tool
obtains symbolic states from Symbolic PathFinder and uses existing algorithms to
infer complex (potentially nonlinear) numerical invariants. Our preliminary
results show that SymInfer is effective in using symbolic states to generate
precise and useful invariants for proving program safety and analyzing program
runtime complexity.  
We also show that SymInfer outperforms existing invariant generation systems.
	}
	}
Downloads: 0