@conference {421, title = {Formally Explaining Neural Network Classification}, booktitle = {FM 2026}, year = {2026}, 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 half-day tutorial will survey 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 will present the existing techniques as instances of a general formalization that allows contrasting them against each other. In addition, we will discuss the issue of the quality of explanations, focusing on their key metrics and factors. After overviewing and contrasting the existing concepts, the tutorial will proceed with presenting a practical framework, SpEXplAIn, which automatically computes Space Explanations, the most general abductionbased 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. Based on real-life case studies from different domains, we will illustrate the usefulness and flexibility of the new proof-based explanation framework.}, url = {https://verify.inf.usi.ch/sites/default/files/papers/paper_373.pdf}, author = {Natasha Sharygina and Faezeh Labbaf and Fabrizio Leopardi and Tom{\'a}{\v s} Kol{\'a}rik and Grigory Fedyukovich and Michael Wand} } @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 {409, title = {CHC-Based Reachability Analysis via Cycle Summarization}, booktitle = {iFM}, year = {2025}, abstract = {Modern reachability analysis techniques are highly effective when applied to software safety verification. However, they still struggle with certain classes of problems, particularly the verification of programs with complex control flow and deep nested loops. In this paper, we introduce Cycle Summarization-based Reachability Analysis (CSRA), a new Constrained Horn Clause (CHC) based approach for reachability analysis of nested-loop software. Our technique relies on the generation and refinement of cycle summaries within the CHC system. CSRA analyzes cycles in a modular manner, constructing summaries and cycle unrollings. Cycle summaries in our approach are used both to prove safety and detect potential safety violations. This enables more efficient exploration of nested loops. The prototype of CSRA is implemented within the Golem CHC solver. An empirical comparison with other reachability analysis techniques demonstrates that our approach is highly competitive in both proving safety and constructing counterexamples.}, author = {Konstantin Britikov and Grigory Fedyukovich and Natasha Sharygina} } @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 {392, title = {Reachability Analysis for Multiloop Programs Using Transition Power Abstraction}, booktitle = {FM 24}, year = {2024}, month = {09/2024}, abstract = {A wide variety of algorithms is employed for the reachability analysis of programs with loops but most of them are restricted to single loop programs. Recently a new technique called Transition Power Abstraction (TPA) showed promising results for safety checks of software. In contrast to many other techniques TPA efficiently handles loops with a large number of iterations. This paper introduces an algorithm that enables the effective use of TPA for analysis of multiloop programs. The TPA-enabled loop analysis reduces the dependency on the number of possible iterations. Our approach analyses loops in a modular manner and both computes and uses transition invariants incrementally, making program analysis efficient. The new algorithm is implemented in the Golem solver. Conducted experiments demonstrate that this approach outperforms the previous implementation of TPA and other competing tools on a wide range of multiloop benchmarks.}, author = {Konstantin Britikov and Martin Blicha and Natasha Sharygina and Grigory Fedyukovich} } @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 {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 {365, title = {Transition Power Abstractions for Deep Counterexample Detection}, booktitle = {TACAS}, year = {2022}, publisher = {Springer LNCS series}, organization = {Springer LNCS series}, abstract = {

While model checking safety of infinite-state systems by inferring state invariants has steadily improved recently, most verification tools still rely on a technique based on bounded model checking to detect safety violations. In particular, the current techniques typically analyze executions by unfolding transitions one step at a time, and the slow growth of execution length prevents detection of deep counterexamples before the tool reaches its limits on computations. We propose a novel model-checking algorithm that is capable of both proving unbounded safety and finding long counterexamples. The idea is to use Craig interpolation to guide the creation of symbolic abstractions of exponentially longer sequences of transitions. Our experimental analysis shows that on unsafe benchmarks with deep counterexamples our implementation can detect faulty executions that are at least an order of magnitude longer than those detectable by the state-of-the-art tools.

}, url = {https://link.springer.com/chapter/10.1007/978-3-030-99524-9_29}, author = {Martin Blicha and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {326, title = {Farkas-Based Tree Interpolation}, booktitle = {SAS 2020 - 27th Static Analysis Symposium}, year = {2020}, publisher = {Springer}, organization = {Springer}, address = {Online Conference}, url = {https://link.springer.com/chapter/10.1007\%2F978-3-030-65474-0_16}, author = {Sepideh Asadi and Martin Blicha and Antti Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina} } @conference {322, title = {Incremental Verification by SMT-based Summary Repair}, booktitle = {20th conference on FORMAL METHODS in COMPUTER-AIDED DESIGN {\textendash} FMCAD 2020}, year = {2020}, publisher = {IEEE digital library, TU Wien Academic Press}, organization = {IEEE digital library, TU Wien Academic Press}, isbn = {978-3-85448-042-6}, url = {http://verify.inf.usi.ch/sites/default/files/upprover-fmcad20.pdf}, author = {Sepideh Asadi and Martin Blicha and Antti E. J. Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina} } @article {351, title = {Exploiting partial variable assignment in interpolation-based model checking.}, journal = {Formal Methods in System Design}, year = {2019}, abstract = {

Craig interpolation has been successfully employed in symbolic program verification as a means of abstraction for sets of program states. In this article, we present the partial variable assignment interpolation system, an extension of the labeled interpolation system, enriched by partial variable assignments. It allows for both generation of smaller interpolants as well as for their faster computation. We present proofs of important properties of the interpolation system as well as a set of experiments proving its usefulness.

}, url = {https://link.springer.com/article/10.1007\%2Fs10703-019-00342-z}, author = {Pavel Jan{\v c}{\'\i}k and Jan Kofron and Leonardo Alt and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {288, title = {Function Summarization Modulo Theories}, booktitle = {22nd International Conference on Logic for Programming Artificial Intelligence and Reasoning, LPAR}, year = {2018}, publisher = {EasyChair Publications}, organization = {EasyChair Publications}, address = {Ethiopia}, keywords = {Author keywords: Software Verification Bounded Model Checking, Craig Interpolation, Function Summaries, Incremental Verification, Satisfiability Modulo Theories, Software Verification}, doi = {10.29007/d3bt}, url = {https://easychair.org/publications/paper/nNLJ}, author = {Sepideh Asadi and Martin Blicha and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Karine Even-Mendoza and Natasha Sharygina and Hana Chockler} } @conference {269, title = {HiFrog: SMT-based Function Summarization for Software Verification}, booktitle = {23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, year = {2017}, publisher = {Springer}, organization = {Springer}, address = {Uppsala}, abstract = {

Abstract. Function summarization can be used as a means of incremental\ verication based on the structure of the program. HiFrog is\ a fully featured function-summarization-based model checker that uses\ SMT as the modeling and summarization language. The tool supports\ three encoding precisions through SMT: uninterpreted functions, linear\ real arithmetics, and propositional logic. In addition the tool allows optimized\ traversal of reachability properties, counter-example-guided summary\ renement, summary compression, and user-provided summaries.\ We describe the use of the tool through the description of its architecture\ and a rich set of features. The description is complemented by an experimental\ evaluation on the practical impact the dierent SMT precisions\ have on model-checking.

}, url = {https://link.springer.com/chapter/10.1007/978-3-662-54580-5_12 }, author = {Leonardo Alt and Sepideh Asadi and Hana Chockler and Karine Even Mendoza and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @proceedings {238, title = {Theory Refinement for Program Verification}, year = {2017}, publisher = {Springer LNCS series}, address = {Melbourne, Australia}, 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.
}, url = {http://verify.inf.usi.ch/hifrog/theoref}, author = {Antti E. J. Hyv{\"a}rinen and Sepideh Asadi and Karine Even Mendoza and Grigory Fedyukovich and Hana Chockler 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 {227, title = {Automated Discovery of Simulation Between Programs}, booktitle = {LPAR}, year = {2015}, author = {Grigory Fedyukovich and Gurfinkel, A. 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 {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 {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} } @conference {202, title = {Towards completeness in Bounded Model Checking through Automatic Recursion Depth Detection}, booktitle = {Brazilian Symposium on Formal Methods (SBMF)}, year = {2014}, address = {Maceio, Brazil.}, author = {Grigory Fedyukovich and Natasha Sharygina} } @conference {190, title = {Verification-Aided Regression Testing}, booktitle = {ISSTA}, year = {2014}, month = {06/2014}, abstract = {

In this paper we present Verification-Aided Regression Testing (VART), a novel extension of regression testing that uses model checking to increase the fault revealing capability of existing test suites. The key idea in VART is to extend the use of test case executions from the conventional direct fault discovery to the generation of behavioral properties specific to the upgrade, by (i) automatically producing properties that are proved to hold for the base version of a program, (ii) automatically identifying and checking on the upgraded program only the properties that, according to the developers{\textquoteright} intention, must be preserved by the upgrade, and (iii) reporting the faults and the corresponding counter-examples that are not revealed by the regression tests. Our empirical study on both open source and industrial software systems shows that VART automatically produces properties that increase the effectiveness of testing by automatically detecting faults unnoticed by the existing regression test suites.\ 

}, author = {Pastore, F. and Mariani, L. and Antti E. J. Hyv{\"a}rinen and Grigory Fedyukovich and Natasha Sharygina and Sehestedt, S. and Muhammad, A.} } @conference { FSS_TACAS13, title = {eVolCheck: Incremental Upgrade Checker for C}, booktitle = {19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, year = {2013}, publisher = {Springer}, organization = {Springer}, author = {Grigory Fedyukovich and Sery, O. and Natasha Sharygina} } @conference {166, title = {Interpolation-based model checking for efficient incremental analysis of software}, booktitle = {IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems}, year = {2013}, author = {Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen 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.} } @conference { Ondrej Sery; Gri, title = {FunFrog: Bounded Model Checking with Interpolation-based Function Summarization}, booktitle = {Tenth International Symposium on Automated Technology for Verification and Analysis (ATVA)}, year = {2012}, note = {To appear at the conference. The pdf-version is not final.}, address = {Thiruvananthapuram, India}, author = {Sery, O. and Grigory Fedyukovich and Natasha Sharygina} } @conference { Ondrej Sery; Gri, title = {Incremental Upgrade Checking by Means of Interpolation-based Function Summaries}, booktitle = {Twelfth International Conference on Formal Methods in Computer-Aided Design (FMCAD)}, year = {2012}, note = {To appear at the conference. The pdf-version is not final.}, address = {Cambridge, UK}, author = {Sery, O. and Grigory Fedyukovich and Natasha Sharygina} } @conference {149, title = {Function Summaries in Software Upgrade Checking}, booktitle = {Haifa Verification Conference (HVC)}, year = {2011}, publisher = {Springer}, organization = {Springer}, address = {Haifa Verification Conference (HVC)}, author = {Grigory Fedyukovich and Sery, O. and Natasha Sharygina} } @conference {148, title = {Interpolation-based Function Summaries in Bounded Model Checking}, booktitle = {Haifa Verification Conference (HVC)}, year = {2011}, publisher = {Springer}, organization = {Springer}, address = {Haifa, Israel}, abstract = {

During model checking of software against various specifications,\ it is often the case that the same parts of the program have to be modeled/verified multiple times.\ To reduce the overall verification effort, this paper proposes a new technique that extracts function summaries after the initial successful verification run,\ and then uses them for more efficient subsequent analysis of the other specifications.\ Function summaries are computed as over-approximations using Craig interpolation, a mechanism which is well-known to preserve the most relevant information,\ and thus tend to be a good substitute for the functions that were examined in the previous verification runs.\ In our summarization-based verification approach, the spurious behaviors introduced as a side effect of the over-approximation,\ are ruled out automatically by means of the counter-example guided refinement of the function summaries.\ We implemented interpolation-based summarization in our FunFrog tool, and compared it with several state-of-the-art software model checking tools.\ Our experiments demonstrate the feasibility of the new technique and confirm its advantages on the large programs.

}, author = {Sery, O. and Grigory Fedyukovich and Natasha Sharygina} }