@proceedings {238,
	title = {Theory Refinement for Program Verification},
	year = {2017},
	publisher = {Springer LNCS series},
	address = {Melbourne, Australia},
	abstract = {<div>
    Recent progress in automated formal verification is to a large degree\&nbsp;due to the development of constraint languages that are sufficiently
light-weight for reasoning but still expressive enough to prove\&nbsp;properties of programs.
Satisfiability modulo theories (SMT) solvers implement efficient\&nbsp;decision procedures, but offer little direct support for adapting the
constraint language to the task at hand.
<em>Theory refinement</em>\&nbsp;is a new approach that modularly adjusts the\&nbsp;modeling precision based on the properties being verified through the
use of\&nbsp;combination\&nbsp;of theories.
We implement the approach using an augmented version of the theory of\&nbsp;bit-vectors and uninterpreted functions capable of directly injecting\&nbsp;non-clausal refinements to the inherent Boolean structure of SMT.
In our comparison to a state-of-the-art model checker, our prototype\&nbsp;implementation is in general competitive, being several orders of
magnitudes faster on some instances that are challenging for flattening,\&nbsp;while computing models that are significantly more succinct.
</div>
},
	url = {http://verify.inf.usi.ch/hifrog/theoref},
	author = {Antti E. J. Hyv{\"a}rinen and Sepideh Asadi and Karine Even Mendoza and Grigory Fedyukovich and Hana Chockler and Natasha Sharygina}
}
