@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.}, 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 {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} } @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 {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 {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} } @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} } @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} } @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} } @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 {150, title = {Lazy Abstraction with Interpolation for Arrays}, booktitle = {18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR)}, year = {2012}, publisher = {Springer}, organization = {Springer}, address = {M{\'e}rida, Venezuela}, abstract = {

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

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

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

}, author = {Francesco Alberti and Bruttomesso, R. and Ghilardi, S. and Ranise, S. and Natasha Sharygina} } @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 {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 {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 {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} }