Martin Blicha

We present PyCHC , a solver-agnostic framework aimed at systems of constrained Horn clauses (CHC). PyCHC provides intuitive Python APIs to create and manipulate CHC systems programmatically, and solve them using different backend solvers. Furthermore, PyCHC offers a certification pipeline to validate the correctness of results reported by the CHC solvers, via the use of independent satisfiability modulo theories (SMT) solvers and proof checkers. We present our framework’s architecture and features, and demonstrate how it enables rapid prototyping of new CHC-based algorithms and experimentation with novel strategies for cooperative solving. We used PyCHC to validate the results of the Eldarica , Golem , and Z3-Spacer solvers on CHC-COMP benchmarks, finding several issues across different tool versions.

Formal verification 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 satisfiability of logic formulas, be it solvers for Boolean satisfiability (SAT), satisfiability modulo theories (SMT), or constrained Horn clauses (CHC). The validation of solvers’ results is thus of paramount importance, in order to increase the confidence not only in the solvers themselves but also in the tooling which they underpin. Among the formalisms commonly used by modern verification tools, CHC is one that has seen, at the same time, extensive practical usage and very little effort in result validation. We propose a two-layered validation approach for witnesses of CHC satisfiability that validates CHC models via proof-backed SMT queries. We developed a modular evaluation framework, ATHENA, and assessed the approach’s viability via large scale experimentation, comparing three CHC solvers, five SMT solvers, and five proof checkers. Our results indicate that the approach is feasible, with the potential to be incorporated into CHC-based tooling, and also confirm the need for validation, with fourteen bugs being found in the tools used.

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 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 state-of-the-art.

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.

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 G olem , a flexible and efficient solver for satisfiability of CHCs over linear real and integer arithmetic. G olem 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 G olem 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.

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.

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 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.

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’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’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.