Explainable Verification Topics

The over-arching goal of our Explainable Verification (pdf) project is to build mathematically principled, practically useful tools for sound static analysis of real programs (primarily C) with a focus on concurrency, explainability, and cooperation between verifiers. This page contains brief descriptions of the tasks that we intend to work on and the essential background readings required to understand the topic.

1. Mathematical foundations

1.1 Modular proofs for thread-modular analyses, via effects. Thread-modular abstract interpretation scales to real concurrent C but the usual proofs lean on tedious history-based arguments. We will recast these proofs to be compositional by structuring the analysis with type-and-effect systems and Dijkstra monads, connecting them back to precise local-trace semantics for concurrency. See thread-modular and local-trace ideas (Schwarz et al. 2021, Schwarz et al. 2023) and effect-based specification and verification (Maillard et al. 2019).

1.2 Foundations of side-effecting constraint systems. Modern scalable analyzers rely on side-effecting constraints to model non-local flows (e.g., interference through globals) and to drive efficient solvers. We will study their mathematical essence using monads, algebraic effects, and handlers so that both generators and solvers become modular objects with clean correctness arguments. Key references include side-effecting constraints (Apinis et al. 2012), monads and effects (Moggi 1991, Plotkin & Power 2002) and handlers in action (Kammar et al. 2013).

1.3 Interactive and incremental analysis. Sound analysis must feel responsive in the IDE. We will combine demanded/incremental abstract interpretation with semantic models of change, such as update monads (Ahman and Uustalu 2013), to limit recomputation and stream stable partial results as the developer edits. See demanded/interactive analysis (Stein et al. 2021, Stein et al. 2024) and our reanalysis prototype (Erhard et al. 2024).

2. Automated software verification algorithms

2.1 Verified solvers for sound program analysis. To increase trust, we will move beyond toy interpreters and verify feature-complete solvers that include widening/narrowing and side effects, using intrinsic (type-and-effect-based) proofs in mainstream proof assistants and F*. Prior work points the way with verified local solvers and abstract interpreters (Hofmann et al. 2010, Franceschino et al. 2021) and practical widening/narrowing schemes (Amato et al. 2016).

2.2 Precise and effective thread-modular abstractions. Real code often synchronizes via heap-allocated or time-based mechanisms that evade existing abstractions. We will develop symbolic/thread-modular abstractions that capture these patterns, guided by graded-effect checks to prune impossible interferences, and integrate them into Goblint, our thread-modular analyzer for C (Vojdani et al. 2016). Background: relational and local-trace concurrency analysis (Miné 2014, Schwarz et al. 2021).

2.3 Witnesses and cooperative verification. Tools should exchange proofs and counterexamples, not just results. We will design/export concurrency-aware witnesses (e.g., rely–guarantee-style invariants) and build validators so other tools can check them, enabling cooperation within frameworks like CoVeriTeam. See witnesses and validation for (mainly) single-threaded verification (Beyer et al. 2015, Beyer et al. 2016) and recent steps toward multi-threaded validation (Saan et al. 2024).

3. Explainable verification in practice

3.1 Explainable abstract interpretation. We aim to generate explanations—consistent with the analyzer’s semantics—for both alarms and proofs of safety, using meta-analyses and optimisation-backed certificates to extract small, human-readable justifications. Background: explanation frameworks for abstract interpretation (Apinis & Vojdani 2023, Cousot et al. 2019) and minimal witness ideas (Funke et al. 2020).

3.2 Practical research on verification user interfaces. We will integrate sound analysis into developer workflows with interactive, debugger-like views over abstract reachability graphs (Holter et al. 2024), and overlays that show “why this warning” and “what would discharge it.” Useful starting points: static-analysis UI design guidelines (Tiganov et al. 2022) and symbolic/temporal debugging metaphors (Karmios et al. 2023, Pasquier et al. 2023).

3.3 Improving benchmarking and evaluation processes. Beyond SV-COMP, we will continuously evaluate on evolving real-world programs, including concurrency-heavy code, and study how witness exchange improves reproducibility. See Goblint’s SV-COMP track records (Saan et al. 2021, Saan et al. 2023) and a representative evaluation of race verification tools (Holter et al. 2025).

How to proceed

If any of the above sounds interesting, contact us with a short note about your background and which WP you’d like to contribute to. We will help scope an MSc project that suits your taste in theory, implementation, and/or evaluation.