@conference {145,
	title = {Flexible Interpolation with Local Proof Transformations},
	booktitle = {International Conference of Computer Aided Design (ICCAD)},
	year = {2010},
	publisher = {IEEE Computer Society},
	organization = {IEEE Computer Society},
	address = {San Jose, USA},
	abstract = {<p><span style="color: rgb(73, 73, 73); font-family: {\textquoteright}Lucida Grande{\textquoteright}, {\textquoteright}Bitstream Vera Sans{\textquoteright}, Arial, sans-serif; ">Model checking based on Craig{\textquoteright}s interpolants ultimately relies on efficient engines, such as SMT-solvers, to log proofs of unsatisfiability and to derive the desired interpolant by means of a set of algorithms known in literature. These algorithms, however, are designed for proofs that do not contain mixed predicates. In this paper we present a technique for transforming the propositional proof produced by an SMT-solver in such a way that mixed predicates are eliminated. We show a number of cases in which mixed predicates arise as a consequence of state-of-the-art solving procedures (e.g. lemma on demand, theory combination, etc.). In such cases our technique can be applied to allow the application of known interpolation algorithms. We demonstrate with a set of experiments that our approach is viable.</span></p>
},
	author = {Bruttomesso, R. and Rollini, S.F. and Natasha Sharygina and Tsitovich, A.}
}
@conference { BPS10,
	title = {A Flexible Schema for Generating Explanations in Lazy Theory Propagation},
	booktitle = {International Conference on Formal Methods and Models for Codesign (MEMOCODE)},
	year = {2010},
	note = {to appear},
	publisher = {IEEE Computer Society},
	organization = {IEEE Computer Society},
	address = {Grenoble, France},
	author = {Bruttomesso, R. and Pek, E. and Natasha Sharygina}
}
