@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 = {

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.

}, 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} }