@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} } @conference {401, title = {Space Explanations of Neural Network Classification}, booktitle = {37th CAV 2025}, year = {2025}, abstract = {We present a novel logic-based concept called Space Explanations for classifying neural networks that gives provable guarantees of the behavior of the network in continuous areas of the input feature space. To automatically generate space explanations, we leverage on a range of flexible Craig interpolation algorithms and unsatisfiable core generation. Based on real-life case studies, ranging from small to medium to large size, we demonstrate that the generated explanations are more meaningful than those computed by the state-of-the-art}, author = {Faezeh Labbaf and Tom{\'a}{\v s} Kol{\'a}rik and Martin Blicha and Grigory Fedyukovich and Michael Wand and Natasha Sharygina} } @conference {390, title = {SolTG: A CHC-based Solidity Test Case Generator}, booktitle = {Computer Aided Verification}, year = {2024}, abstract = {

Test coverage is an important metric for the development of blockchain smart contracts. In this paper, we present SolTG, an automated CHC-based test case generator for Solidity smart contracts. SolTG exhaustively enumerates symbolic formulas and makes calls to SMT solver to find input values under which the contract exhibits the corresponding behavior. Test cases synthesized by SolTG have the form of a sequence of function calls over concrete values of input parameters, which lead to a specific execution scenario. The tool supports multiple Solidity-specific features and is capable of generating high coverage for industrial-grade Solidity code. We present a detailed architecture of SolTG and the translation of smart contracts into their CHC representation that the tool relies on. We also present the experimental results for test generation on the regression and industrial benchmarks.

}, url = {https://link.springer.com/content/pdf/10.1007/978-3-031-65627-9_23.pdf}, author = {Konstantin Britikov and Ilia Zlatkin and Grigory Fedyukovich and Leonardo Alt and Natasha Sharygina} } @article {379, title = {SMT-based verification of program changes through summary repair}, journal = {Formal Methods in System Design}, year = {2023}, month = {05/2023}, abstract = {This article provides an innovative approach for verification by model checking of programs that undergo continuous changes. To tackle the problem of repeating the entire model checking for each new version of the program, our approach verifies programs incrementally. It reuses computational history of the previous program version, namely function summaries. In particular, the summaries are over-approximations of the bounded program behaviors. Whenever reusing of summaries is not possible straight away, our algorithm repairs the summaries to maximize the chance of reusability of them for subsequent runs. We base our approach on satisfiability modulo theories (SMT) to take full advantage of lightweight modeling approach and at the same time the ability to provide concise function summarization. Our approach leverages pre-computed function summaries in SMT to localize the checks of changed functions. Furthermore, to exploit the trade-off between precision and performance, our approach relies on the use of an SMT solver, not only for underlying reasoning, but also for program modeling and the adjustment of its precision. On the benchmark suite of primarily Linux device drivers versions, we demonstrate that our algorithm achieves an order of magnitude speedup compared to prior approaches.}, doi = {https://doi.org/10.1007/s10703-023-00423-0}, url = {https://link.springer.com/epdf/10.1007/s10703-023-00423-0?sharing_token=irB5EyKrDQwFBGsATR5X_Pe4RwlQNchNByi7wbcMAY69DCBPoCd5OukXnJUT4hJ-i8lTSfPkBgFCDWhP5zZ6F07I66RayboKJEpVSax8y-1gkPqsTej9UbMHSNiNQ_jERujVnNQQ7kvxuZcpsB3rGMYcHJEINXClhcP3Ttz85V4=}, author = {Sepideh Asadi and Martin Blicha and Antti E. J. Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina} } @conference {375, title = {Symbolic Model Checking for TLA+ Made Faster}, booktitle = {TACAS - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, year = {2023}, address = {Paris}, url = {https://doi.org/10.1007/978-3-031-30823-9_7}, author = {Rodrigo Otoni and Igor Konnov and Jure Kukovec and Patrick Eugster and Natasha Sharygina} } @conference {369, title = {SolCMC: Solidity Compiler{\textquoteright}s Model Checker}, booktitle = {CAV}, year = {2022}, address = { Haifa, Isreal}, abstract = {

Formally verifying smart contracts is important due to their immutable nature, usual open source licenses, and high financial incentives for exploits. Since 2019 the Ethereum Foundation{\textquoteright}s Solidity compiler ships with a model checker. The checker, called SolCMC, has two different reasoning engines and tracks closely the development of the Solidity language. We describe SolCMC{\textquoteright}s architecture and use from the perspective of developers of both smart contracts and tools for software verification, and show how to analyze nontrivial properties of real life contracts in a fully automated manner.

}, keywords = {SolCMC}, author = {Leonardo Alt and Martin Blicha and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @article {373, title = {A Solicitous Approach to Smart Contract Verification}, journal = {ACM Transactions on Privacy and Security}, year = {2022}, type = {Full-Length Research Paper}, url = {https://dl.acm.org/doi/10.1145/3564699}, author = {Rodrigo Otoni and Matteo Marescotti and Leonardo Alt and Patrick Eugster and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {372, title = {Split Transition Power Abstraction for Unbounded Safety}, year = {2022}, abstract = {

Transition Power Abstraction (TPA) is a recent sym- bolic model checking approach that leverages Craig interpolation to create a sequence of symbolic abstractions for transition paths that double in length with each new element. This doubling abstraction allows the approach to find bugs that require long executions much faster than traditional approaches that unfold transitions one at a time, but its ability to prove system safety is limited. This paper proposes a novel instantiation of the TPA approach capable of proving unbounded safety efficiently while preserving the unique capability to detect deep counterexamples. The idea is to split the transition over-approximations in two complementary parts. One part focuses only on reachability in fixed number of steps, the second part complements it by summarizing all shorter paths. The resulting split abstractions are suitable for discovering safe transition invariants, making the SPLIT-TPA approach much more efficient in proving safety and even improving the counterexample detection. The approach is implemented in the constrained Horn clause solver GOLEM and our experimental comparison against state-of-the-art solvers shows it to be both competitive and complementary.

}, author = {Martin Blicha and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {300, title = {{SMTS:} Distributed, Visualized Constraint Solving}, booktitle = {{LPAR-22.} 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018}, year = {2018}, author = {Matteo Marescotti and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {232, title = {Search-Space Partitioning for Parallelizing SMT Solvers}, booktitle = {MEMICS2015}, year = {2015}, url = {http://verify.inf.usi.ch/sites/default/files/memics2015.pdf}, author = {Matteo Marescotti and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {223, title = {Search-Space Partitioning for Parallelizing SMT Solvers}, booktitle = {SAT 2015}, year = {2015}, author = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Natasha Sharygina} } @mastersthesis {219, title = {An SMT-based verification framework for software systems handling arrays}, volume = {PhD}, year = {2015}, month = {02/2015}, pages = {188}, school = {Universit{\`a} della Svizzera Italiana}, type = {Doctoral Dissertation}, address = {Lugano}, url = {http://www.falberti.it/thesis/phd.pdf}, author = {Francesco Alberti} } @conference {208, title = {Symbolic Detection of Assertion Dependencies for Bounded Model Checking}, booktitle = {18th International Conference on Fundamental Approaches to Software Engineering (FASE)}, year = {2015}, author = {Grigory Fedyukovich and Callia D{\textquoteright}Iddio, A. and Antti E. J. Hyv{\"a}rinen 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} } @mastersthesis { Aliaksei Tsitovi, title = {Scalable Abstractions for Efficient Security Checks}, year = {2011}, pages = {164}, school = {University of Lugano}, type = {PhD Thesis}, address = {Lugano}, author = {Aliaksei Tsitovich} } @conference {142, title = {A Scalable Decision Procedure for Fixed-Width Bit-Vectors}, booktitle = {International Conference of Computer Aided Design (ICCAD)}, year = {2009}, publisher = {ACM}, organization = {ACM}, address = {San Jose (CA)}, author = {Bruttomesso, R. and Natasha Sharygina} } @conference {156, title = {The Synergy of Precise and Fast Abstractions for Program Verification}, booktitle = {24th Annual ACM Symposium on Applied Computing (SAC)}, year = {2009}, publisher = {ACM}, organization = {ACM}, address = {Honolulu, USA}, abstract = {

Predicate abstraction is a powerful technique to reduce the state space of a program to a finite and affordable number of states. It produces a conservative over-approximation where concrete states are grouped together according to the predicates. Given a set of predicates, a precise abstraction contains the minimal set of transitions, but as a result is computationally expensive. Most model checkers therefore approximate the abstraction to alleviate the computation of the abstract system by trading off precision with cost. However, approximation results in a higher number of refinement iterations, since it can produce more false counterexamples than its precise counterpart. The refinement loop can become prohibitively expensive for large programs.

This paper proposes a new abstraction refinement technique that combines slow and precise predicate abstraction techniques with fast and imprecise ones. It allows computing the abstraction quickly, but keeps it precise enough to avoid too many refinement iterations. We implemented the new algorithm in a state-of-the-art software model checker. Our tests with various real life benchmarks show that the new approach systematically outperforms both precise and imprecise techniques.

}, author = {Natasha Sharygina and Tonetta, S. and Tsitovich, A.} }