@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.
	}
	}

{"_id":"oyGJJjSHttnuNg58Y","bibbaseid":"nguyen-dwyer-visser-syminferinferringprograminvariantsusingsymbolicstates-2017","downloads":0,"creationDate":"2017-10-28T07:45:41.382Z","title":"SymInfer: Inferring Program Invariants using Symbolic States","author_short":["Nguyen, T.","Dwyer, M.","Visser, W."],"year":2017,"bibtype":"inproceedings","biburl":"http://cse.unl.edu/~tnguyen/vu_bibs1.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Nguyen"],"firstnames":["ThanhVu"],"suffixes":[]},{"propositions":[],"lastnames":["Dwyer"],"firstnames":["Matthew"],"suffixes":[]},{"propositions":[],"lastnames":["Visser"],"firstnames":["William"],"suffixes":[]}],"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. ","bibtex":"@inproceedings{symtracesase17,\n\tAuthor = {Nguyen, ThanhVu and Dwyer, Matthew and Visser, William},\n\tBooktitle = {Automated Software Engineering (ASE)},\n\tPublisher = {IEEE},\n\tPages = {to appear},\n\tBibbase_Note = {},\n\tTitle = {{SymInfer: Inferring Program Invariants using Symbolic States}},\n Url_paper = {Pub/symtraces.pdf},\n\tUrl_slides = {Pub/symtraces_pres.pdf},\t\t\t\n\tUrl_code = {https://bitbucket.org/nguyenthanhvuh/symtraces/},\n\tYear = {2017},\n\tAbstract = {\nWe introduce a new technique for inferring program invariants that uses symbolic\nstates generated by symbolic execution. Symbolic states,\nwhich consist of path conditions and constraints on local variables, \nare a compact description of sets of concrete program states and they\ncan be used for both invariant inference and invariant verification. \nOur technique uses a\ncounterexample-based algorithm that creates\nconcrete states from symbolic states, infers candidate\ninvariants from concrete states, and then verifies or refutes candidate\ninvariants using symbolic states. The refutation case produces concrete\ncounterexamples that prevent spurious results and allow the technique to\nobtain more precise invariants. This process stops when the algorithm reaches\na stable set of invariants.\n\nWe present SymInfer, a tool that implements these ideas to automatically\ngenerate invariants at arbitrary locations in a Java program. The tool\nobtains symbolic states from Symbolic PathFinder and uses existing algorithms to\ninfer complex (potentially nonlinear) numerical invariants. Our preliminary\nresults show that SymInfer is effective in using symbolic states to generate\nprecise and useful invariants for proving program safety and analyzing program\nruntime complexity. \nWe also show that SymInfer outperforms existing invariant generation systems.\n\t}\n\t}\n\n\n","author_short":["Nguyen, T.","Dwyer, M.","Visser, W."],"key":"symtracesase17","id":"symtracesase17","bibbaseid":"nguyen-dwyer-visser-syminferinferringprograminvariantsusingsymbolicstates-2017","role":"author","urls":{" paper":"http://cse.unl.edu/~tnguyen/Pub/symtraces.pdf"," slides":"http://cse.unl.edu/~tnguyen/Pub/symtraces_pres.pdf"," code":"https://bitbucket.org/nguyenthanhvuh/symtraces/"},"downloads":0},"search_terms":["syminfer","inferring","program","invariants","using","symbolic","states","nguyen","dwyer","visser"],"keywords":[],"authorIDs":["545748b32abc8e9f3700025d"],"dataSources":["AAQcbSuJRTAKBGbG3"]}