@conference {326,
	title = {Farkas-Based Tree Interpolation},
	booktitle = {SAS 2020 - 27th Static Analysis Symposium},
	year = {2020},
	publisher = {Springer},
	organization = {Springer},
	address = {Online Conference},
	url = {https://link.springer.com/chapter/10.1007\%2F978-3-030-65474-0_16},
	author = {Sepideh Asadi and Martin Blicha and Antti Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina}
}
@conference {288,
	title = {Function Summarization Modulo Theories},
	booktitle = {22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR},
	year = {2018},
	publisher = {EasyChair Publications},
	organization = {EasyChair Publications},
	address = {Ethiopia},
	keywords = {Author keywords:	 Software Verification Bounded Model Checking, Craig Interpolation, Function Summaries, Incremental Verification, Satisfiability Modulo Theories, Software Verification},
	doi = {10.29007/d3bt},
	url = {https://easychair.org/publications/paper/nNLJ},
	author = {Sepideh Asadi and Martin Blicha and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Karine Even-Mendoza and Natasha Sharygina and Hana Chockler}
}
@conference {248,
	title = {Flexible Interpolation for Efficient Model Checking},
	booktitle = {MEMICS 2016},
	year = {2016},
	url = {http://verify.inf.usi.ch/sites/default/files/MEMICS2016.pdf},
	author = {Antti E. J. Hyv{\"a}rinen and Leonardo Alt and Natasha Sharygina}
}
@conference { Ondrej Sery; Gri,
	title = {FunFrog: Bounded Model Checking with Interpolation-based Function Summarization},
	booktitle = {Tenth International Symposium on Automated Technology for Verification and Analysis (ATVA)},
	year = {2012},
	note = {To appear at the conference. The pdf-version is not final.},
	address = {Thiruvananthapuram, India},
	author = {Sery, O. and Grigory Fedyukovich and Natasha Sharygina}
}
@conference {149,
	title = {Function Summaries in Software Upgrade Checking},
	booktitle = {Haifa Verification Conference (HVC)},
	year = {2011},
	publisher = {Springer},
	organization = {Springer},
	address = {Haifa Verification Conference (HVC)},
	author = {Grigory Fedyukovich and Sery, O. and Natasha Sharygina}
}
@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}
}
