@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 {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} } @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} }