Effective Automated Software Verification: A Multilayered Approach

You are cordially invited to attend the PhD Dissertation Defence of Martin Blicha on Tuesday 21 March 2023 at 08:15 in room D0.02 (USI East campus).

Abstract:
Automated software verification decides correctness of a given program with respect to a given formal specification. Formal verification techniques based on model checking provide the necessary guarantees by exploring program’s behaviour exhaustively and automatically. Even though the general problem that automated software verification is trying to solve is undecidable, it is quite efficient on many instances that arise in practice. However, significant challenges related to scalability persist for complex modern programs. In our work, we argue that this task can be approached by providing solutions at different levels, which we identify as foundational, verification and cooperative layers of the problem. These correspond to decision and interpolation procedures, sequential model-checking algorithms, and multi-agent solving approaches. We further argue that working on the higher layers can significantly benefit from a deep understanding of the layers beneath them. Overall, we advance the field of automated software verification by contributing solutions on all three layers. On the foundational layer, we contribute a new interpolation algorithm for conflicts in the theory of linear arithmetic. It extends the standard approach based on the Farkas lemma and can compute logically stronger interpolants. Experimental evaluation in a model-checking scenario shows that with our interpolation algorithm, the same model-checking algorithm can successfully solve some problems on which it diverges using the original interpolation algorithm. On the verification layer, we invent the concept of transition power abstraction sequence and contribute TPA-based model-checking algorithms that address the known problem of detecting deep counterexamples in transition systems. Moreover, we show that the TPA sequence can be mined for candidates for transition invariants. This allows TPA-based algorithms to prove systems safe by means largely orthogonal to existing techniques. To support the development of verification techniques, we contribute GOLEM, a new solver for the satisfiability of systems of constrained Horn clauses. The main features of GOLEM are its tight integration with the underlying interpolating SMT solver and support for multiple back-end solving algorithms. On the cooperative layer, we contribute an abstract framework generalizing concepts from induction-based model-checking algorithms. The abstraction aims explicitly at the application in a multi-agent solving scenario where multiple instances of the same solver exchange information and, in this way, cooperate to solve a single problem instance. We instantiate the framework to obtain a parallel version of a successful PD-KIND algorithm and experimentally show that exchanging information can significantly improve performance. Since PD-KIND relies on interpolation as a sub-procedure, we use our novel interpolation algorithm to obtain more diverse behaviour of the agents, and this constitutes a large part of the performance improvement.

Dissertation Committee:

• Prof. Natasha Sharygina, Università della Svizzera italiana, Switzerland (Research Advisor)
• Prof. Jan Kofron, Charles University, Czech Republic (Research co-Advisor)
• Prof. Patrick Thomas Eugster, Università della Svizzera italiana, Switzerland (Internal Member)
• Prof. Matthias Hauswirth, Università della Svizzera italiana, Switzerland (Internal Member)
• Prof. Nikolaj Bjørner, Microsoft Research, U.S.A (External Member)
• Prof. Pavel Parizek, Charles University, Czech Republic (External Member)
• Prof. Philipp Rümmer, Uppsala University, Sweden (External Member)