@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 {415, title = {Interpreting Logical Explanations of Classifying Neural Networks}, booktitle = {ESANN 2026}, year = {2026}, abstract = {Formal methods are routinely used to address the issue of explainability of machine learning models. Yet, it is not always trivial to understand how a logical explanation could be useful in practice due to human readability challenges. This paper applies classical geometric methods for interpreting logical explanations and illustrates the usefulness for the users on datasets from medical and image classification domains previously studied in the context of formal explainability.}, url = {https://verify.inf.usi.ch/sites/default/files/papers/ESANN.pdf}, author = {Fabrizio Leopardi and Faezeh Labbaf and Tom{\'a}{\v s} Kol{\'a}rik and Michael Wand and Natasha Sharygina} } @conference {416, title = {Parallel SMT Solving via Iterative Tree Partitioning}, booktitle = {TACAS 2026}, year = {2026}, abstract = {We present a novel algorithm for parallel solving of SMT problems based on a partitioning process that divides the original problem into a tree structure in an iterative way. By enabling node revisiting, the new method addresses the problem of partitioning divergence found in prior approaches that frequently leads to longer runtimes compared to sequential results. The resulting algorithm is highly flexible, offers a combination of partitioning, portfolio solving, and clause sharing, allows the use of various partitioning functions, and scales gracefully with the available resources. We implemented the new approach in the tool SMTS on top of the efficient sequential SMT solver OpenSMT. Our experimental results demonstrate a substantial improvement over OpenSMT in logics QF LRA and QF LIA even when the partitioning approach utilizes just a single solver. Notably, SMTS has consistently dominated several divisions of the annual competition of parallel SMT solvers.}, author = {Tom{\'a}{\v s} Kol{\'a}rik and Antti E. J. Hyv{\"a}rinen and Seyedmasoud Asadzadeh and Natasha Sharygina} } @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} } @article {399, title = {Golem: a flexible and efficient solver for constrained Horn clauses}, journal = {Formal Methods in System Design}, year = {2025}, abstract = {The logical framework of Constrained Horn Clauses (CHC) models verification tasks from a variety of domains, ranging from verification of safety properties in transition systems to modular verification of programs with procedures. In this work we present Golem, a flexible and efficient solver for satisfiability of CHCs over linear real and integer arithmetic. Golem provides flexibility with modular architecture and multiple back-end model-checking algorithms, as well as efficiency with tight integration with the underlying SMT solver. This paper describes the architecture of Golem and its back-end engines, which include our recently introduced model-checking algorithm TPA for deep exploration. The description is complemented by extensive evaluation, demonstrating the competitive nature of the solver.}, doi = {https://doi.org/10.1007/s10703-025-00470-9}, url = {https://rdcu.be/efgv8}, author = {Martin Blicha and Konstantin Britikov 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 {403, title = {Unsatisfiability Proofs for Horn Solving}, booktitle = {TACAS}, year = {2025}, abstract = {Many verification tools currently rely on logic solvers as backend reasoning engines. Despite playing such a pivotal role, bugs are not uncommon in the complex codebases of these solvers. Validating their results is thus critical, with correctness witnesses often being used for this end. Output validation for constrained Horn clauses (CHC) solvers is not a well explored topic though, especially in regards to unsatisfiability results. This is a significant issue, given that CHC solvers are being increasingly employed in verification tooling. To address it, we propose an approach to validate CHC unsatisfiability results based on independently checkable proofs. Our approach is generic in regards to the solving algorithm, preprocessing steps, and exact proof format used, and works by first producing a coarse-grained proof during solving and then instantiating it into a suitable proof format by adding missing details, at which point the instantiated proof can be checked by an independent proof checker. We instrumented a state-of-the-art CHC solver to generate proofs in the Alethe format and performed a large-scale evaluation. Our results indicate that proofs can be produced with minimal overhead, can be efficiently checked, and have tractable sizes. }, doi = {10.1007/978-3-031-90653-4_4}, author = {Rodrigo Otoni and Martin Blicha and Matias Barandiaran Rivera and Patrick Eugster and Jan Kofron and Natasha Sharygina} } @conference {405, title = {Validation of CHC Satisfiability with ATHENA}, year = {2025}, abstract = {Formal veriication tooling increasingly relies on logic solvers as automated reasoning engines. A commonality among these solvers is the high complexity of their codebases, which makes bug occurrence disturbingly frequent. Tool competitions have showcased many examples of state-of-the-art solvers disagreeing on the satisiability of logic formulas, be it solvers for Boolean satisiability (SAT), satisiability modulo theories (SMT), or constrained Horn clauses (CHC). The validation of solvers{\textquoteright} results is thus of paramount importance, in order to increase the conidence not only in the solvers themselves, but also in the tooling which they underpin. Among the formalisms commonly used by modern veriication tools, CHC is one that has seen, at the same time, extensive practical usage and very little eforts in result validation. We propose a two-layered validation approach for witnesses of CHC satisiability that validates CHC models via proof-backed SMT queries. We developed a modular evaluation framework, ATHENA, and assessed the approach{\textquoteright}s viability via large scale experimentation, comparing three CHC solvers, ive SMT solvers, and ive proof checkers. Our results indicate that the approach is feasible, with potential to be incorporated into CHC-based tooling, and also conirm the need for validation, with fourteen bugs being found in the tools used.}, url = {https://dl.acm.org/doi/10.1145/3716505}, author = {Otoni Rodrigo and Blicha Martin and Eugster Patrick and Sharygina Natasha} } @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} } @conference {383, title = {CHC Model Validation with Proof Guarantees}, booktitle = {18th International Conference on integrated Formal Methods (iFM23)}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-47705-8_4}, author = {Rodrigo Otoni and Martin Blicha and Patrick Eugster and Natasha Sharygina} } @conference {382, title = {The Golem Horn Solver}, booktitle = {Computer Aided Verification}, year = {2023}, abstract = {The logical framework of Constrained Horn Clauses (CHC) models verification tasks from a variety of domains, ranging from verifi- cation of safety properties in transition systems to modular verification of programs with procedures. In this work we present Golem, a flexible and efficient solver for satisfiability of CHC over linear real and integer arithmetic. Golem provides flexibility with modular architecture and multiple back-end model-checking algorithms, as well as efficiency with tight integration with the underlying SMT solver. This paper describes the architecture of Golem and its back-end engines, which include our recently introduced model-checking algorithm TPA for deep exploration. The description is complemented by extensive evaluation, demonstrating the competitive nature of the solver.}, doi = {https://doi.org/10.1007/978-3-031-37703-7\_10}, url = {https://verify.inf.usi.ch/sites/default/files/cav23-final109.pdf}, author = {Martin Blicha and Konstantin Britikov and Natasha Sharygina} } @conference {387, title = {Picky CDCL: SMT-solving With Flexible Literal Selection}, booktitle = {VSTTE}, year = {2023}, abstract = {SMT solvers have traditionally been optimized for determining the satisfiability of a query as quickly as possible. However, they are increasingly being used in applications where the time required to determine satisfiability might not be the main concern, such as mining inductive invariants for safety proofs. This paper studies how lookahead-inspired SMT solving, when made sufficiently efficient and integrated into a conflict-driven, clause learning SMT core, can be a valuable component in a portfolio for proof-based interpolation in model checking. We implemented the algorithmic idea, called Picky CDCL, in the SMT solver OpenSMT and show its efficiency in the Horn solver Golem using a range of model checking approaches and in SMT proof validation applications.}, url = {https://link.springer.com/chapter/10.1007/978-3-031-66064-1_1}, author = {Konstantin I. Britikov and Antti E. J. Hyv{\"a}rinen 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 {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 {358, title = {Lookahead in Partitioning SMT}, booktitle = {Formal Methods in Computer-Aided Design - FMCAD 2021}, year = {2021}, publisher = {IEEE digital library}, organization = {IEEE digital library}, address = {Online Conference}, abstract = {

Lookahead in propositional satisfiability has proven efficient as a heuristic in pre- and in-processing, for partitioning instances for parallel solving, and as the main driver of a standalone solver. While applying similar techniques in satisfiability modulo theories is potentially equally useful, adapting lookahead to learning theory clauses and to estimating search space sizes in the presence of first-order structures is not straightforward. This paper addresses both of these observations. We give a hybrid algorithm that integrates lookahead into the state-based representation of an SMT solver and show that in the vast majority of cases it is possible to compute full lookahead up to depth four on inexpensive theories. We also show the role of first-order structures in SMT search space: while in most of our benchmarks the partitions are easier to solve than the original instance, we identify cases where lookahead results in sequences of increasingly difficult instances for a computationally expensive theory.

}, author = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Natasha Sharygina} } @conference {334, title = {Theory-Specific Proof Steps Witnessing Correctness of SMT Executions}, booktitle = {DAC 2021 - 58th Design Automation Conference}, year = {2021}, month = {11/2021}, publisher = {IEEE}, organization = {IEEE}, address = {San Francisco, CA, USA}, doi = {10.1109/DAC18074.2021.9586272}, author = {Rodrigo Otoni and Martin Blicha and Patrick Eugster and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @article {356, title = {Using linear algebra in decomposition of Farkas interpolants}, journal = {International Journal on Software Tools for Technology Transfer}, year = {2021}, type = {Journal}, abstract = {

The use of propositional logic and systems of linear inequalities over reals is a common means to model software for formal verification. Craig interpolants constitute a central building block in this setting for over-approximating reachable states, e.g. as candidates for inductive loop invariants. Interpolants for a linear system can be efficiently computed from a Simplex refutation by applying the Farkas{\textquoteright} lemma. However, these interpolants do not always suit the verification task{\textemdash}in the worst case, they can even prevent the verification algorithm from converging. This work introduces the decomposed interpolants, a fundamental extension of the Farkas interpolants, obtained by identifying and separating independent components from the interpolant structure, using methods from linear algebra. We also present an efficient polynomial algorithm to compute decomposed interpolants and analyse its properties. We experimentally show that the use of decomposed interpolants in model checking results in immediate convergence on instances where state-of-the-art approaches diverge. Moreover, since being based on the efficient Simplex method, the approach is very competitive in general.

}, url = {https://link.springer.com/article/10.1007/s10009-021-00641-z}, author = {Martin Blicha and Antti E. J. Hyv{\"a}rinen and Jan Kofron and Natasha Sharygina} } @conference {319, title = {Accurate Smart Contract Verification through Direct Modelling}, booktitle = {ISoLA 2020 - 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation}, year = {2020}, publisher = {Springer International Publishing}, organization = {Springer International Publishing}, isbn = {978-3-030-61467-6}, doi = {doi.org/10.1007/978-3-030-61467-6_12}, url = {https://link.springer.com/chapter/10.1007\%2F978-3-030-61467-6_12}, author = {Matteo Marescotti and Rodrigo Otoni and Leonardo Alt and Patrick Eugster and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @conference {310, title = {A Cooperative Parallelization Approach for Property-Directed k-Induction}, booktitle = {VMCAI 2020 - 21st International Conference on Verification, Model Checking, and Abstract Interpretation}, year = {2020}, address = { New Orleans, USA, 19-25 January 2020}, doi = {10.1007/978-3-030-39322-9_13}, author = {Martin Blicha and Antti E. J. Hyv{\"a}rinen and Matteo Marescotti 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} } @mastersthesis {332, title = {Parallelization and modelling techniques for scalable SMT-based verification}, volume = {PhD}, year = {2020}, month = {01.12.2020}, school = {USI Lugano}, abstract = {

Software systems are increasingly involved in our daily life tasks, making their failures potentially damaging both in economic and human terms. As a result, proving the correctness of software is widely thought to be one of the most central challenges for computer science. Model checking is an award-winning (Turing award, 2007) technique for formally and automatically verifying systems, often capable to guarantee the correctness of non-trivial and practical programs. However, model checking is undecidable in the general case. Even when properly restricted to the decidable fragment, the algorithms face strong scalability issues preventing them to converge to the solution. The goal of this thesis is to address such scalability issues in two orthogonal ways. First, the design of parallel solving techniques that exploit the massive amount of computational power offered by distributed computing environments. Second, the design of a modelling technique for effective verification of the new emergent technology of smart contracts running on blockchain systems. The parallel solving research efforts consider both bounded and induction-based unbounded model checking, respectively achieved by instantiating multi-agent solving for the T-DPLL and IC3 algorithms. Multi-agent techniques leverage on the diversification and cooperation among sequential solvers executed in parallel. Diversification is achieved with different parallel search heuristics, and cooperation is performed with the exchange of information both during solving time and via upfront agreements. The effectivenesses of various multi-agent settings are empirically evaluated using the purpose-built multi-agent framework SMTS. Verification approaches for emerging technologies tend to either reuse tools for existing languages that often result in inefficient and even unsound models, or to apply generic techniques which typically require human intervention to succeed. This thesis provides a new direct modelling approach using constrained Horn clauses for the emerging technology of smart contracts. Such approach allows automatic solving exploiting the proposed efforts in improving inductive solvers scalability, and guarantees soundness for the safety proofs. Additionally, the smart-contracts-specific task of measuring the amount of computation needed to execute a transaction, i.e. gas consumption, is considered in this thesis proposing an algorithmic solution. The effectiveness of the modelling technique is empirically evaluated over smart contracts deployed in the Ethereum blockchain using an implementation inside the official compiler for the smart contracts language Solidity that relies on the IC3 algorithm.

}, url = {http://verify.inf.usi.ch/sites/default/files/phd_thesis_matteo_marescotti.pdf}, author = {Matteo Marescotti} } @conference {298, title = {Decomposing Farkas Interpolants}, booktitle = {TACAS}, year = {2019}, author = {Martin Blicha and Antti E. J. Hyv{\"a}rinen and Jan Kofron 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 {353, title = {Lattice-based SMT for program verification}, booktitle = {International Conference on Formal Methods and Models for System Design, (MEMOCODE)}, year = {2019}, publisher = {ACM-IEEE}, organization = {ACM-IEEE}, abstract = {

We present a lattice-based satisfiability modulo theory for verification of programs with library functions, for which the mathematical libraries supporting these functions contain a high number of equations and inequalities. Common strategies for dealing with library functions include treating them as uninterpreted functions or using the theories under which the functions are fully defined. The full definition could in most cases lead to instances that are too large to solve efficiently. Our lightweight theory uses lattices for efficient representation of library functions by a subset of guarded literals. These lattices are constructed from equations and inequalities of properties of the library functions. These subsets are found during the lattice traversal. We generalise the method to a number of lattices for functions whose values depend on each other in the program, and we describe a simultaneous traversal algorithm of several lattices, so that a combination of guarded literals from all lattices does not lead to contradictory values of their variables. We evaluate our approach on benchmarks taken from the robotics community, and our experimental results demonstrate that we are able to solve a number of instances that were previously unsolvable by existing SMT solvers.

}, url = {https://dl.acm.org/doi/10.1145/3359986.3361214}, author = {Karine Even Mendoza and Antti E. J. Hyv{\"a}rinen and Hana Chockler and Natasha Sharygina} } @conference {293, title = {Computing Exact Worst-Case Gas Consumption for Smart Contracts}, booktitle = {International Symposium on Leveraging Applications of Formal Methods ISoLA 2018: Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice }, year = {2018}, publisher = {Springer}, organization = {Springer}, address = {Cyprus}, abstract = {

The Ethereum platform is a public, distributed, blockchain-based database that is maintained by independent parties. A user interacts with Ethereum by writing programs and having miners execute them for a fee charged on-the-fly based on the complexity of the execution. The exact fee, measured in gas consumption, in general depends on the unknown Ethereum state, and predicting even its worst case is in principle undecidable. Uncertainty in gas consumption may result in inefficiency, loss of money, and, in extreme cases, in funds being locked for an indeterminate duration. This feasibility study presents two methods for determining the exact worst-case gas consumption of a bounded Ethereum execution using methods influenced by symbolic model checking. We give several concrete cases where gas consumption estimation is needed, and provide two approaches for determining gas consumption, one based on symbolically enumerating execution paths, and the other based on computing paths modularly based on the program structure.

}, doi = {doi.org/10.1007/978-3-030-03427-6_33}, url = {https://link.springer.com/chapter/10.1007\%2F978-3-030-03427-6_33}, author = {Matteo Marescotti and Martin Blicha and Antti E. J. Hyv{\"a}rinen and Sepideh Asadi 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 {287, title = {Lattice-Based Refinement in Bounded Model Checking}, booktitle = {VSTTE}, year = {2018}, month = {07/2018}, author = {Karine Even-Mendoza and Sepideh Asadi and Antti Hyv{\"a}rinen and Hana Chockler and Natasha Sharygina} } @conference {290, title = {Lookahead-Based SMT Solving}, booktitle = {LPAR-22}, year = {2018}, month = {November 2018}, publisher = {EasyChair}, organization = {EasyChair}, address = {Awassa, Ethiopia}, url = {http://www.inf.usi.ch/postdoc/hyvarinen/publications/HyvarinenMSCS_LPAR2018.pdf}, author = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Parvin Sadigova and Hana Chockler and Natasha Sharygina} } @book {355, title = {Modeling for Verification}, series = {Handbook of Model Checking}, year = {2018}, publisher = {Springer}, organization = {Springer}, abstract = {

System modeling is the initial, and often crucial, step in verification. The right choice of model and modeling language is important for both designers and users of verification tools. This chapter aims to provide a guide to system modeling in four stages. First, it provides an overview of the main issues one must consider in modeling systems for verification. These issues involve both the selection or design of a modeling language and the steps of model creation. Next, it introduces a simple modeling language, sml, for illustrating the issues involved in selecting or designing a modeling language. sml uses an abstract state machine formalism that captures key features of widely-used languages based on transition system representations. We introduce the simple modeling language to simplify the connection between languages used by practitioners (such as Verilog, Simulink, or C) and various underlying formalisms (e.g., automata or Kripke structures) used in model checking. Third, the chapter demonstrates key steps in model creation using sml with illustrative examples. Finally, the presented modeling language sml is mapped to standard formalisms such as Kripke structures.

}, url = {https://link.springer.com/chapter/10.1007\%2F978-3-319-10575-8_3}, author = {Sanjit A. Seshia and Natasha Sharygina and Stavros Tripakis} } @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 {277, title = {Duality-Based Interpolation for Quantifier-Free Equalities and Uninterpreted Functions}, booktitle = {17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017) }, year = {2017}, publisher = {IEEE XPlore and ACM Digital Libraries}, organization = {IEEE XPlore and ACM Digital Libraries}, address = {TU Wien, Vienna, Austria,}, url = {http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD17/fmcad17_proceedings.pdf}, author = {Leonardo Alt and Antti Hyv{\"a}rinen and Sepideh Asadi and Natasha Sharygina} } @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} } @conference {279, title = {LRA Interpolants from No Man{\textquoteright}s Land}, booktitle = {Haifa Verification Conference (HVC)}, year = {2017}, publisher = {Springer{\textquoteright}s Lecture Notes in Computer Science series (LNCS)}, organization = {Springer{\textquoteright}s Lecture Notes in Computer Science series (LNCS)}, author = {Leonardo Alt 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} } @conference {250, title = {Clause Sharing and Partitioning for Cloud-Based SMT Solving}, booktitle = {ATVA 2016}, year = {2016}, url = {http://verify.inf.usi.ch/sites/default/files/ATVA2016.pdf}, author = {Matteo Marescotti and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina} } @proceedings {246, title = {Combining parallel techniques for Cloud-Based SMT Solving}, year = {2016}, url = {http://verify.inf.usi.ch/sites/default/files/PhD-iFM2016.pdf}, author = {Matteo Marescotti} } @conference {248, title = {Flexible Interpolation for Efficient Model Checking}, booktitle = {MEMICS 2016}, year = {2016}, url = {http://verify.inf.usi.ch/sites/default/files/MEMICS2016.pdf}, author = {Antti E. J. Hyv{\"a}rinen and Leonardo Alt and Natasha Sharygina} } @conference {335, title = {OpenSMT2: An SMT Solver for Multi-Core and Cloud Computing}, year = {2016}, author = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Leonardo Alt 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} } @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 {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 {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 {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} } @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 {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 {194, title = {VERIGE: Verification with Invariant Generation Engine}, booktitle = {SPIN}, year = {2014}, publisher = {ACM}, organization = {ACM}, author = {Latorre, N. and Francesco Alberti 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 { 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 {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 {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} } @article {164, title = {Loop summarization using state and transition invariants}, journal = {Formal Methods in System Design}, volume = {42}, year = {2013}, issn = {0925-9856}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} } @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} } @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.} } @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} } @article { Natasha Sharygin, title = {An abstraction refinement approach combining precise and approximated techniques}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {14}, year = {2012}, pages = {1-14}, publisher = {Springer}, keywords = {Approximated abstraction, CEGAR, Precise abstraction, Predicate abstraction}, url = {http://dx.doi.org/10.1007/s10009-011-0185-y}, author = {Natasha Sharygina and Tonetta, S. and Tsitovich, A.} } @article {340, title = {An abstraction refinement approach combining precise and approximated techniques}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {14}, year = {2012}, 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 a given set of predicates. A precise abstraction contains the minimal set of transitions with regard to the predicates, 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 approach that employs both precise (slow) and approximated (fast) abstraction techniques within one abstraction-refinement loop. 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 almost systematically outperforms both precise and imprecise techniques.

}, url = {https://link.springer.com/article/10.1007/s10009-011-0185-y}, author = {Natasha Sharygina and Stefano Tonetta and Aliaksei Tsitovich} } @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 {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 {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 {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} } @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} } @conference { twks11, title = {Loop Summarization and Termination Analysis}, booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {6605}, year = {2011}, pages = {81-95}, publisher = {Springer}, organization = {Springer}, address = {Saarbr{\"u} Germany}, url = {http://dx.doi.org/10.1007/978-3-642-19835-9_9}, author = {Aliaksei Tsitovich and Natasha Sharygina and Christoph M. Wintersteiger and Kroening, Daniel} } @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 {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.} } @conference { BPS10, title = {A Flexible Schema for Generating Explanations in Lazy Theory Propagation}, booktitle = {International Conference on Formal Methods and Models for Codesign (MEMOCODE)}, year = {2010}, note = {to appear}, publisher = {IEEE Computer Society}, organization = {IEEE Computer Society}, address = {Grenoble, France}, author = {Bruttomesso, R. and Pek, E. and Natasha Sharygina} } @article { BSB10, title = {A Model Checking-based Approach for Security Policy Verification of Mobile Systems}, journal = {Formal Aspects of Computing Journal}, year = {2010}, note = {to appear}, publisher = {Springer}, author = {Braghin, C. and Natasha Sharygina and Katerina Barone Adesi} } @conference { BPST10, title = {The OpenSMT Solver}, booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {6015}, year = {2010}, pages = {150-153}, publisher = {Springer}, organization = {Springer}, address = {Paphos, Cyprus}, url = {http://dx.doi.org/10.1007/978-3-642-12002-2_12}, author = {Bruttomesso, R. and Pek, E. and Natasha Sharygina and Tsitovich, A.} } @conference {154, title = {Termination Analysis with Compositional Transition Invariants}, booktitle = {International Conference on Computer-Aided Verification (CAV)}, year = {2010}, publisher = {Springer}, organization = {Springer}, address = {Edinburgh, UK}, abstract = {

Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check\ is known to be the bottleneck of the procedure. We present an alternative algorithm that uses a light-weight check based on transitivity of\ ranking relations to prove program termination. We provide an experimental evaluation over a set of 87 Windows drivers, and demonstrate\ that our algorithm is often able to conclude termination by examining\ only a small fraction of the program. As a consequence, our algorithm is\ able to outperform known approaches by multiple orders of magnitude.\ 

}, author = {Kroening, D. and Natasha Sharygina and Tsitovich, A. and Wintersteiger, C.M.} } @conference {143, title = {An Extension of the Davis-Putnam Procedure and its Application to Preprocessing in SMT}, booktitle = {7th International Workshop on Satisfiability Modulo Theories (SMT)}, year = {2009}, publisher = {ACM}, organization = {ACM}, address = {Montreal, Canada}, author = {Bruttomesso, R.} } @conference {153, title = {Loopfrog: A Static Analyzer for ANSI-C Programs}, booktitle = {The 24th IEEE/ACM International Conference on Automated Software Engineering}, year = {2009}, publisher = {IEEE Computer Society}, organization = {IEEE Computer Society}, address = {Auckland, New Zealand}, abstract = {

Practical software verification is dominated by two major classes of techniques. The first is model checking, which provides total precision, but suffers from the state space explosion problem. The second is abstract interpretation, which is usually much less demanding, but often returns a high number of false positives.

We present Loopfrog, a static analyzer that combines the best of both worlds: the precision of model checking and the performance of abstract interpretation. In contrast to traditional static analyzers, it also provides "leaping" counterexamples to aid in the diagnosis of errors.

}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} } @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.} } @conference {155, title = {Detection of Security Vulnerabilities Using Guided Model Checking}, booktitle = {24th International Conference on Logic Programming (ICLP)}, year = {2008}, publisher = {Springer}, organization = {Springer}, address = {Udine, Italy}, author = {Tsitovich, A.} } @conference {152, title = {Loop Summarization using Abstract Transformers}, booktitle = {6th International Symposium on Automated Technology for Verification and Analysis (ATVA)}, year = {2008}, publisher = {Springer, Volume 5311}, organization = {Springer, Volume 5311}, address = {Seoul, South Korea}, abstract = {

Existing program analysis tools that implement abstraction rely on saturating procedures to compute over-approximations of fixpoints. As an alternative, we propose a new algorithm to compute an over-approximation of the set of reachable states of a program by replacing loops in the control flow graph by their abstract transformer. Our technique is able to generate diagnostic information in case of property violations, which we call leaping counterexamples. We have implemented this technique and report experimental results on a set of large ANSI-C programs using abstract domains that focus on properties related to string-buffers.

}, author = {Kroening, D. and Natasha Sharygina and Tonetta, S. and Tsitovich, A. and Wintersteiger, C.M.} } @conference {157, title = {Automated Verification of Security Policies in Mobile Code.}, booktitle = {Integrated Formal Methods (IFM)}, year = {2007}, publisher = {Springer, Volume 4591}, organization = {Springer, Volume 4591}, abstract = {

This paper describes an approach for the automated verification of mobile programs. Mobile systems are characterized by the explicit notion of locations (e.g., sites where they run) and the ability to execute at different locations, yielding a number of security issues. We give formal semantics to mobile systems as Labeled Kripke Structures, which encapsulate the notion of the location net. The location net summarizes the hierarchical nesting of threads constituting a mobile program and enables specifying security policies. We formalize a language for specifying security policies and show how mobile programs can be exhaustively analyzed against any given security policy by using model checking techniques.
We developed and experimented with a prototype framework for analysis of mobile code, using the SATABS model checker. Our approach relies on SATABS{\textquoteright}s support for unbounded thread creation and enhances it with location net abstractions, which are essential for verifying large mobile programs. Our experimental results on various benchmarks are encouraging and demonstrate advantages of the model checking-based approach, which combines the validation of security properties with other checks, such as for buffer overflows.

}, author = {Braghin, C. and Natasha Sharygina and Katerina Barone Adesi} }