The 13th edition of the Competition on Software Verification (SV-COMP 2024) was the
largest competition of its kind so far: A total of 76 tools for verification and witness validation …

The 12th edition of the Competition on Software Verification (SV-COMP 2023) is again the
largest overview of tools for software verification, evaluating 52 verification systems from 34 …

Bubaak-SpLit is a tool for dynamically splitting verification tasks into parts that can then be
analyzed in parallel. It is built on top of Bubaak, a tool designed for running combinations of …

Memory models allow reasoning about the correctness of multithreaded programs.
Constructing and using such models is facilitated by simulators that reveal which behaviours …

AISE is a static verifier that can verify the safety properties of C programs. The core of AISE is
a program verification framework that synergizes abstract interpretation and symbolic …

When verifiers report an alarm, they export a violation witness (exchangeable
counterexample) that helps validate the reachability of that alarm. Conventional wisdom …

Six years ago, we performed the first large-scale comparison of automated test generators
and software model checkers with respect to bug-finding capabilities on a benchmark set …

Software verification tools automatically prove the correctness of programs with respect to
user supplied specifications. Today, such tools implement a range of different types of …

The distributed programming framework for parallel graph computation has been proposed
to process and analyze large scale graph data. However, how to model and verify properties …

This thesis aims to develop efficient, mathematically sound methods to improve software
reliability using abstract interpretation, a formal framework for approximating program …