@conference {387, title = {Picky CDCL: SMT-solving With Flexible Literal Selection}, booktitle = {VSTTE}, year = {2023}, abstract = {SMT solvers have traditionally been optimized for determining the satisfiability of a query as quickly as possible. However, they are increasingly being used in applications where the time required to determine satisfiability might not be the main concern, such as mining inductive invariants for safety proofs. This paper studies how lookahead-inspired SMT solving, when made sufficiently efficient and integrated into a conflict-driven, clause learning SMT core, can be a valuable component in a portfolio for proof-based interpolation in model checking. We implemented the algorithmic idea, called Picky CDCL, in the SMT solver OpenSMT and show its efficiency in the Horn solver Golem using a range of model checking approaches and in SMT proof validation applications.}, author = {Konstantin I. Britikov and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @proceedings {240, title = {Property Directed Equivalence via Abstract Simulation}, year = {2016}, author = {Grigory Fedyukovich and Gurfinkel, A. and Natasha Sharygina} } @conference {234, title = {PVAIR: Partial Variable Assignment InterpolatoR}, booktitle = {FASE2016}, year = {2016}, url = {http://verify.inf.usi.ch/sites/default/files/main-2.pdf}, author = {Pavel Jan{\v c}{\'\i}k and Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Jan Kofron and Natasha Sharygina} } @conference {222, title = {A Proof-Sensitive Approach for Small Propositional Interpolants}, booktitle = {VSTTE 2015}, year = {2015}, url = {http://verify.inf.usi.ch/sites/default/files/main_0.pdf}, author = {Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {160, title = {A Parametric Interpolation Framework for First-Order Theories}, booktitle = {12th Mexican International Conference on Artificial Intelligence (MICAI)}, year = {2013}, author = {Kovacs, L. and Rollini, S.F. and Natasha Sharygina} } @conference {180, title = {PeRIPLO: A Framework for Producing Efficient Interpolants for SAT-based Software Verification}, booktitle = {Logic for Programming Artificial Intelligence and Reasoning (LPAR)}, year = {2013}, address = {Stellenbosch, South Africa}, author = {Rollini, S.F. and Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {165, title = {PINCETTE - Validating Changes and Upgrades in Networked Software}, booktitle = {17th European Conference on Software Maintenance and Reengineering}, year = {2013}, author = {Chockler, H. and Denaro, G. and Ling, M. and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Mariani, L. and Muhammad, A. and Oriol, M. and Rajan, A. and Sery, O. and Natasha Sharygina and Tautschnig, M.} }