Natasha Sharygina

FM Conference 2026 Conference Paper

Formally Explaining Neural Network Classification

• Tomáš Kolárik
• Grigory Fedyukovich
• Faezeh Labbaf
• Fabrizio Leopardi
• Natasha Sharygina
• Michael Wand

Abstract Neural networks (NNs) are the core of AI-based technologies. However, the degree of reliability in performing the task is an open problem. The explainability of a central task of NNs, classification, is of immense importance. While at the rise of AI-based reasoning, explainability of the NN classification has mostly been done using statistical methods, nowadays, a more reliable trend of formal logic-based methods is gaining popularity. The advantage of the formal approach is that it gives strict and provable guarantees of the classification. Formal methods is a mature field that has delivered a number of efficient computational solutions already applied in the analysis of software and hardware systems. Formal explainability methods naturally have the ability to reuse existing techniques and tools for a newly emerging field of formal explainability of NN classification. This paper surveys existing efforts to compute explanations of neural network classification based on logical abductive reasoning. The abduction approach is crucial for generalizing the results, capturing the underlying behavior of the classifier. We present the existing techniques as instances of a general formalization that allows contrasting them against each other. In addition, we discuss the issue of the quality of explanations, focusing on their key metrics and factors. As an illustrative example, the paper also presents a practical framework, SpEXplAIn, which automatically computes Space Explanations, the most general abduction-based explanations for classifying NNs with provable guarantees of the behavior of the network in continuous areas of the input feature space. The tool leverages an SMT solver compatible with a range of flexible Craig interpolation algorithms and unsatisfiable core generation, and is applicable to a wide range of applications.

TACAS Conference 2026 Conference Paper

Parallel SMT Solving via Iterative Tree Partitioning

• Tomáš Kolárik
• Antti E. J. Hyvärinen
• Seyedmasoud Asadzadeh
• Natasha Sharygina

LPAR Conference 2018 Conference Paper

Function Summarization Modulo Theories

• Sepideh Asadi
• Martin Blicha
• Grigory Fedyukovich
• Antti E. J. Hyvärinen
• Karine Even-Mendoza
• Natasha Sharygina
• Hana Chockler

SMT-based program verification can achieve high precision using bit-precise models or combinations of different theories. Often such approaches suffer from problems related to scalability due to the complexity of the underlying decision procedures. Precision is traded for performance by increasing the abstraction level of the model. As the level of abstraction increases, missing important details of the program model becomes problematic. In this paper we address this problem with an incremental verification approach that alternates precision of the program modules on demand. The idea is to model a program using the lightest possible (i. e. , less expensive) theories that suffice to verify the desired property. To this end, we employ safe over-approximations for the program based on both function summaries and light-weight SMT theories. If during verification it turns out that the precision is too low, our approach lazily strengthens all affected summaries or the theory through an iterative refinement procedure. The resulting summarization framework provides a natural and light-weight approach for carrying information between different theories. An experimental evaluation with a bounded model checker for C on a wide range of benchmarks demonstrates that our approach scales well, often effortlessly solving instances where the state-of-the-art model checker CBMC runs out of time or memory.

LPAR Conference 2018 Conference Paper

Lookahead-Based SMT Solving

• Antti E. J. Hyvärinen
• Matteo Marescotti
• Parvin Sadigova
• Hana Chockler
• Natasha Sharygina

The lookahead approach for binary-tree-based search in constraint solving favors branching that provide the lowest upper bound for the remaining search space. The approach has recently been applied in instance partitioning in divide-and-conquer-based parallelization, but in general its connection to modern, clause-learning solvers is poorly understood. We show two ways of combining lookahead approach with a modern DPLL(T)-based SMT solver fully profiting from theory propagation, clause learning, and restarts. Our thoroughly tested prototype implementation is surprisingly efficient as an independent SMT solver on certain instances, in particular when applied to a non-convex theory, where the lookahead-based implementation solves 40% more unsatisfiable instances compared to the standard implementation.

LPAR Conference 2018 Conference Paper

SMTS: Distributed, Visualized Constraint Solving

• Matteo Marescotti
• Antti E. J. Hyvärinen
• Natasha Sharygina

The inherent complexity of parallel computing makes development, resource monitor- ing, and debugging for parallel constraint-solving-based applications difficult. This paper presents SMTS, a framework for parallelizing sequential constraint solving algorithms and running them in distributed computing environments. The design (i) is based on a gen- eral parallelization technique that supports recursively combining algorithm portfolios and divide-and-conquer with the exchange of learned information, (ii) provides monitoring by visually inspecting the parallel execution steps, and (iii) supports interactive guidance of the algorithm through a web interface. We report positive experiences on instantiating the framework for one SMT solver and one IC3 solver, debugging parallel executions, and visualizing solving, structure, and learned clauses of SMT instances.

SAT Conference 2017 Conference Paper

Theory Refinement for Program Verification

• Antti E. J. Hyvärinen
• Sepideh Asadi
• Karine Even-Mendoza
• Grigory Fedyukovich
• Hana Chockler
• Natasha Sharygina

Abstract Recent progress in automated formal verification is to a large degree due to the development of constraint languages that are sufficiently light-weight for reasoning but still expressive enough to prove properties of programs. Satisfiability modulo theories (SMT) solvers implement efficient decision procedures, but offer little direct support for adapting the constraint language to the task at hand. Theory refinement is a new approach that modularly adjusts the modeling precision based on the properties being verified through the use of combination of theories. We implement the approach using an augmented version of the theory of bit-vectors and uninterpreted functions capable of directly injecting non-clausal refinements to the inherent Boolean structure of SMT. In our comparison to a state-of-the-art model checker, our prototype implementation is in general competitive, being several orders of magnitudes faster on some instances that are challenging for flattening, while computing models that are significantly more succinct.

SAT Conference 2016 Conference Paper

OpenSMT2: An SMT Solver for Multi-core and Cloud Computing

• Antti E. J. Hyvärinen
• Matteo Marescotti
• Leonardo Alt
• Natasha Sharygina

Abstract This paper describes a major revision of the OpenSMT solver developed since 2008. The version 2 significantly improves its predecessor by providing a design that supports extensions, several critical bug fixes and performance improvements. The distinguishing feature of the new version is the support for a wide range of parallelization algorithms both on multi-core and cloud-computing environments. Presently the solver implements the quantifier free theories of uninterpreted functions and equalities and linear real arithmetics, and is released under the MIT license.

LPAR Conference 2015 Conference Paper

Automated Discovery of Simulation Between Programs

• Grigory Fedyukovich
• Arie Gurfinkel
• Natasha Sharygina

Abstract The paper presents SimAbs, the first fully automated SMT-based approach to synthesize an abstraction of one program (called target) that simulates another program (called source). SimAbs iteratively traverses the search space of existential abstractions of the target and choses the strongest abstraction among them that simulates the source. Deciding whether a given relation is a simulation relation is reduced to solving validity of \(\forall \exists \) -formulas iteratively. We present a novel algorithm for dealing with such formulas using an incremental SMT solver. In addition to deciding validity, our algorithm extracts witnessing Skolem relations which further drive simulation synthesis in SimAbs. Our evaluation confirms that SimAbs is able to efficiently discover both, simulations and abstractions, for C programs from the Software Verification Competition.

SAT Conference 2015 Conference Paper

Search-Space Partitioning for Parallelizing SMT Solvers

• Antti E. J. Hyvärinen
• Matteo Marescotti
• Natasha Sharygina

Abstract This paper studies how parallel computing can be used to reduce the time required to solve instances of the Satisfiability Modulo Theories problem (SMT). We address the problem in two orthogonal ways: (i) by distributing the computation using algorithm portfolios, search space partitioning techniques, and their combinations; and (ii) by studying the effect of partitioning heuristics, and in particular the lookahead heuristic, to the efficiency of the partitioning. We implemented the approaches in the OpenSMT2 solver and experimented with the QF_UF theory on a computing cloud. The results show a consistent speed-up on hard instances with up to an order of magnitude run time reduction and more instances being solved within the timeout compared to the sequential implementation.

LPAR Conference 2013 Conference Paper

PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification

• Simone Fulvio Rollini
• Leonardo Alt
• Grigory Fedyukovich
• Antti E. J. Hyvärinen
• Natasha Sharygina

Abstract Propositional interpolation is widely used as a means of overapproximation to achieve efficient SAT-based symbolic model checking. Different verification applications exploit interpolants for different purposes; it is unlikely that a single interpolation procedure could provide interpolants fit for all cases. This paper describes the PeRIPLO framework, an interpolating SAT-solver that implements a set of techniques to generate and manipulate interpolants for different model checking tasks. We demonstrate the flexibility of the framework in two software bounded model checking applications: verification of a given source code incrementally with respect to various properties, and verification of software upgrades with respect to a fixed set of properties. Both applications use interpolation for generating function summaries. Our systematic experimental investigation shows that size and logical strength of interpolants significantly affect verification, that these characteristics depend on the role played by interpolants, and that therefore techniques for tuning size and strength can be used to customize interpolants in different applications.

LPAR Conference 2012 Conference Paper

Lazy Abstraction with Interpolants for Arrays

• Francesco Alberti
• Roberto Bruttomesso
• Silvio Ghilardi
• Silvio Ranise
• Natasha Sharygina

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 and prove universally quantified properties over arrays in a completely automatic fashion.

TCS Journal 2007 Journal Article

Verification of Boolean programs with unbounded thread creation

• Byron Cook
• Daniel Kroening
• Natasha Sharygina

Most symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. Boolean programs [T. Ball, S. K. Rajamani, Bebop: A symbolic model checker for Boolean programs, in: SPIN 00, in: Lecture Notes in Computer Science, vol. 1885, Springer, 2000, pp. 113–130] are the most popular representation for these abstractions. Unfortunately, today’s symbolic software model checkers are limited to the analysis of sequential programs due to the fact that reachability in Boolean programs with unbounded thread creation is undecidable. We address this limitation with a novel algorithm for over-approximating reachability in Boolean programs with unbounded thread creation. Although the Boolean programs are not of finite state, the algorithm always reaches a fix-point. The fixed points are detected by projecting the state of the threads to the globally visible parts, which are finite.