@conference {210, title = {On Interpolants and Variable Assignments}, booktitle = {Formal Methods in Computer-Aided Design (FMCAD)}, year = {2014}, address = {Lausanne, Switzerland}, author = {Jancik, P. and KofronĖ‡, J. and Rollini, S.F. 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} } @article {168, title = {Resolution Proof Transformation for Compression and Interpolation}, journal = {CoRR}, volume = {July 2013}, year = {2013}, author = {Rollini, S.F. and Bruttomesso, R. and Natasha Sharygina and Tsitovich, A.} } @conference {159, title = {Using Cross-Entropy for Satisfiability}, booktitle = {ACM Symposium on Applied Computing (SAC)}, year = {2013}, author = {Chockler, H. and Ivrii, A. and Matsliah, A. and Rollini, S.F. and Natasha Sharygina} } @conference {146, title = {Leveraging Interpolant Strength in Model Checking}, booktitle = {24th International Conference on Computer Aided Verification (CAV)}, year = {2012}, publisher = {Springer}, organization = {Springer}, address = {Berkeley, California, USA}, abstract = {

Craig interpolation is a well known method of abstraction successfully used in both hardware and software model checking. The logical strength of interpolants can affect the quality of approximations and consequently the performance of the model checkers. Recently, it was observed that for the same resolution proof a complete lattice of interpolants ordered by strength can be derived.
Most state-of-the-art model checking techniques based on interpolation subject the interpolants to constraints that ensure efficient verification as, for example, in transition relation approximation for bounded model checking, counterexample-guided abstraction refinement and function summarization for software update checking. However, in general, these verification-specific constraints are not satisfied by all possible interpolants.
The paper analyzes the restrictions within the lattice of interpolants under which the required constraints are satisfied. This enables investigation of the effect of the strength of interpolants on the particular techniques, while preserving their soundness. As an additional benefit, combination of this result with proof manipulation procedures allows the use of optimized solvers to generate interpolants of different strengths for various model checking techniques.

}, author = {Rollini, S.F. and Sery, O. and Natasha Sharygina} } @conference {144, title = {An Efficient and Flexible Approach to Resolution Proof Reduction}, booktitle = {Haifa Verification Conference (HVC)}, year = {2010}, publisher = {Springer}, organization = {Springer}, address = {Haifa, Israel}, abstract = {

A propositional proof of unsatisfiability is a certificate of the\ unsatisfiability of a Boolean formula. Resolution proofs, as generated by\ modern SAT solvers, find application in many verification techniques\ where the size of the proofs considerably affects efficiency. This paper\ presents a new approach to proof reduction, situated among the purely\ post-processing methods. The main idea is to reduce the proof size by\ eliminating redundancies of occurrences of pivots along the proof paths.\ This is achieved by matching and rewriting local contexts into simpler\ ones. In our approach, rewriting can be easily customized in the way\ local contexts are matched, in the amount of transformations to be performed, or in the different application of the rewriting rules. We provide\ an extensive experimental evaluation of our technique on a set of SMT\ benchmarks, which shows considerable reduction in the proofs size.

}, author = {Rollini, S.F. and Bruttomesso, R. 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.} }