@conference {417, title = {Syntactically Convex Model-Based Projection for Linear Real Arithmetic}, booktitle = {TACAS 2026}, year = {2026}, abstract = {Quantifier elimination (QE) is a key task in formal verification algorithms, and the ability to return partial results, such as under-approximations, is beneficial for many QE clients. In Linear Real Arithmetic (LRA), existing QE methods often fail to preserve syntactic convexity, that is, they return a disjunction even for a conjunctive input, or they return a large non-minimal representation. We define the novel concept of Bidirectional Model-Based Projection and a new QE algorithm for LRA (BMBP-QE) that (i) returns a conjunctive over-approximation and a disjunctive under-approximation when interrupted early, (ii) returns a minimal conjunction when the input is conjunctive, and (iii) applies to arbitrary LRA formulae. We show that BMBP-QE outperforms SMT-based QE algorithms, offering improvements in both runtime and result size.}, author = {Anna Becchi and Grigory Fedyukovich and Arie Gurfinkel and Lev Nachmanson} } @proceedings {240, title = {Property Directed Equivalence via Abstract Simulation}, year = {2016}, author = {Grigory Fedyukovich and Gurfinkel, A. and Natasha Sharygina} } @conference {227, title = {Automated Discovery of Simulation Between Programs}, booktitle = {LPAR}, year = {2015}, author = {Grigory Fedyukovich and Gurfinkel, A. and Natasha Sharygina} } @article {216, title = {Decision Procedures for Flat Array Properties}, journal = {J. Autom. Reasoning}, volume = {54}, year = {2015}, month = {04/2015}, pages = {352}, chapter = {327}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @conference {221, title = {A new Acceleration-based Combination Framework for Array Properties}, booktitle = {FROCOS 2015}, year = {2015}, author = {Francesco Alberti and Silvio Ghilardi and Natasha Sharygina} } @conference {185, title = {Decision Procedures for Flat Array Properties}, booktitle = {TACAS}, year = {2014}, publisher = {Springer}, organization = {Springer}, address = {Grenoble, France}, abstract = {
We present new decidability results for quantified fragments\ of theories of arrays. Our decision procedures are fully declarative, parametric in the theories of indexes and elements and orthogonal with respect to known results. We also discuss applications to the analysis of\ programs handling arrays.
}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @article {193, title = {An extension of lazy abstraction with interpolation for programs with arrays}, journal = {FMSD}, year = {2014}, keywords = {Array programs, Lazy abstraction, Model checking, SMT}, issn = {1572-8102}, doi = {10.1007/s10703-014-0209-9}, author = {Francesco Alberti and Bruttomesso, R. and Ghilardi, S. and Ranise, S. and Natasha Sharygina} } @conference {183, title = {Incremental Verification of Compiler Optimizations}, booktitle = {NASA Formal Methods (NFM)}, year = {2014}, address = {Houston, Texas, USA}, abstract = {
Optimizations are widely used along the lifecycle of software.\ However, proving the equivalence between original and optimized versions is difficult. In this paper, we propose a technique to incrementally\ verify different versions of a program with respect to a fixed property. We\ exploit a safety proof of a program given by a safe inductive invariant.\ For each optimization, such invariants are adapted to be a valid safety\ proof of the optimized program (if possible). The cost of the adaptation depends on the impact of the optimization and is often less than\ an entire re-verification of the optimized program. We have developed a\ preliminary implementation of our technique in the context of Software\ Model Checking. Our evaluation of the technique on different classes of\ industrial programs and standard LLVM optimizations confirms that the\ optimized programs can be re-verified efficiently.
}, author = {Grigory Fedyukovich and Gurfinkel, A. and Natasha Sharygina} } @article {173, title = {Abstraction and Acceleration in SMT-based Model-Checking for Array Programs}, journal = {CoRR}, volume = {April 2013}, year = {2013}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @conference {167, title = {Definability of Accelerated Relations in a Theory of Arrays and Its Applications}, booktitle = {Frontiers of Combining Systems}, year = {2013}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} } @conference {147, title = {Interpolation Properties and SAT-based Model Checking}, booktitle = {11th International Symposium on Automated Technology for Verification and Analysis (ATVA)}, year = {2013}, author = {Gurfinkel, A. and Rollini, S. F. and Natasha Sharygina} } @conference {150, title = {Lazy Abstraction with Interpolation for Arrays}, booktitle = {18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR)}, year = {2012}, publisher = {Springer}, organization = {Springer}, address = {M{\'e}rida, Venezuela}, abstract = {

Lazy abstraction with interpolants has been shown to be a powerful technique for verifying imperative programs. In presence of arrays, however, the method shows an intrinsic limitation, due to the fact that successful invariants usually contain universally quantified variables, which are not present in the program specification. In this work we present an extension of the interpolation-based lazy abstraction in which arrays of unknown length can be handled in a natural manner. In particular, we exploit the Model Checking Modulo Theories framework to derive a backward reachability version of lazy abstraction that embeds array reasoning. The approach is generic, in that it is valid for both parameterized systems and imperative programs. We show by means of experiments that our approach can synthesize an prove universally quantified properties over arrays in a completely automatic fashion.

}, author = {Francesco Alberti and Bruttomesso, R. and Ghilardi, S. and Ranise, S. and Natasha Sharygina} } @conference {151, title = {SAFARI: SMT-based Abstraction For Arrays with Interpolants}, booktitle = {24th International Conference on Computer Aided Verification (CAV)}, year = {2012}, publisher = {Springer}, organization = {Springer}, address = {Berkeley, California, USA}, abstract = {

We present SAFARI, a model checker designed to prove (possibly universally quantified) safety properties of imperative programs with arrays of unknown length. SAFARI is based on an extension of lazy abstraction capable of handling existentially quantified formul{\ae} for symbolically representing states. A heuristics, called term abstraction, favors the convergence of the tool by {\textquotedblleft}tuning{\textquotedblright} interpolants and guessing additional quantified variables of invariants to prune the search space efficiently.

}, author = {Francesco Alberti and Bruttomesso, R. and Ghilardi, S. and Ranise, S. and Natasha Sharygina} }