HEXAGONbeta

Voblint: End-to-End Soundness of a Context-Sensitive Goblint-Style Analyzer in Isabelle/HOL

A mix of human-written and AI-generated textHuman understanding: all partscs.LO — Logic in Computer Science

Contributed by Manuel Lerchner ↗

Version 1 / Nov 05, 2026 / CC BY 4.0

Abstract

Goblint-style analyzers solve side-effecting equations, where evaluating one unknown can contribute to other unknowns. An existing Isabelle/HOL proof establishes solver partial correctness without connecting the equations to execution. We mechanize this connection for a scalar imperative language with recursive procedures but no pointers or heap memory. We adapt the local traces of Schwarz et al. to record procedure activations and the callers resumed by returns. A context policy relates concrete calls to one or more analysis contexts. A cover assigns sets of stores to program points and contexts as candidate overapproximations of reachability. We prove that five local obligations suffice for a cover to contain every valid trace’s final store in every admitted context, on any control-flow graph. A post-solution assigns abstract values that bound each equation’s result and side effects. When the abstract operations are sound and the routing agrees with the context policy, every post-solution induces a cover. The verified solver computes a post-solution when it returns. For every accepted configuration, whenever the Isabelle-defined analyzer returns a report, it overapproximates the stores reached by finite source executions from the prescribed initial states. Whenever execution reaches a check, PROVED guarantees that its condition holds, and REFUTED guarantees that it fails. Neither verdict establishes reachability. This source-level guarantee applies to the Isabelle-defined analyzer; solver termination, parsing, and correctness of generated code are not established.

Provenance statement

The author extensively used Anthropic's Claude, OpenAI's ChatGPT and Codex, and Cursor. Under the author's supervision, these tools produced a large share of the implementation. This included Isabelle proofs after definitions and interfaces stabilized, cross-theory refactorings, and conversions of tactic-style proofs to structured Isar. They helped adapt the local traces of Schwarz et al. to procedure activations and refine the trace requirements. Agents wrote much of the command-line interface, regression corpus, and consistency tooling. The author chose the research direction, selected and revised designs, and approved definitions and theorem statements; Isabelle checked every proof. The tools also assisted with literature search and drafting and revising the text and figures, which the author reviewed. Grammarly checked spelling and grammar.

Tools used

Isabelle
IsabelleVersion 2025-2
Anthropic
Claude
OpenAI
ChatGPT

References

  1. Kalmer Apinis; Helmut Seidl; Vesal Vojdani. Side-Effecting Constraint Systems: A Swiss Army Knife for Program Analysis. Programming Languages and Systems (APLAS 2012), vol. 7705, pp. 157–172. 2012DOI
  2. Clemens Ballarin. Locales: A Module System for Mathematical Theories. Journal of Automated Reasoning, vol. 52, no. 2, pp. 123–153. 2014DOI
  3. Sandrine Blazy; Vincent Laporte; André Maroneze; David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. Static Analysis, pp. 324–344. 2013DOI
  4. Joachim Breitner. Shivers' Control Flow Analysis. Archive of Formal Proofs. 2010link
  5. David Cachera; Thomas Jensen; David Pichardie; Vlad Rusu. Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science, vol. 342, no. 1, pp. 56–78. 2005DOI
  6. David Cachera; David Pichardie. A Certified Denotational Abstract Interpreter. Interactive Theorem Proving (ITP 2010), pp. 9–24. 2010DOI
  7. Frédéric Dabrowski; David Pichardie. A Certified Data Race Analysis for a Java-like Language. Theorem Proving in Higher Order Logics (TPHOLs 2009), pp. 212–227. 2009DOI
  8. Paulo Emílio de Vilhena; François Pottier; Jacques-Henri Jourdan. Spy Game: Verifying a Local Generic Solver in Iris. Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, pp. 33:1–33:28. 2020DOI
  9. Lucas Franceschino; David Pichardie; Jean-Pierre Talpin. Verified Functional Programming of an Abstract Interpreter. Static Analysis (SAS 2021), pp. 124–143. 2021. Hosted browser version: https://w95psp.github.io/verified-abstract-interpreterDOI
  10. Florian Haftmann; Tobias Nipkow. Code Generation via Higher-Order Rewrite Systems. Functional and Logic Programming (FLOPS 2010), vol. 6009, pp. 103–117. 2010DOI
Show all 39 referencesShow fewer references
  1. Martin Hofmann; Aleksandr Karbyshev; Helmut Seidl. Verifying a Local Generic Solver in Coq. Static Analysis (SAS 2010), pp. 340–355. 2010DOI
  2. David Van Horn; Matthew Might. Abstracting Abstract Machines. Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 51–62. 2010DOI
  3. Brian Huffman; Ondřej Kunčar. Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. Certified Programs and Proofs (CPP 2013), pp. 131–146. 2013DOI
  4. Bertrand Jeannet; Wendelin Serwe. Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs. Algebraic Methodology and Software Technology (AMAST 2004), vol. 3116, pp. 258–273. 2004DOI
  5. Jacques-Henri Jourdan; Vincent Laporte; Sandrine Blazy; Xavier Leroy; David Pichardie. A Formally-Verified C Static Analyzer. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 247–259. 2015DOI
  6. Jens Knoop; Bernhard Steffen. The Interprocedural Coincidence Theorem. Compiler Construction (CC '92), vol. 641, pp. 125–140. 1992DOI
  7. Peter Lammich; Markus Müller-Olm. Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors. Archive of Formal Proofs. 2007link
  8. Manuel Lerchner. Voblint: A Verified Goblint-Style Static Analysis Pipeline in Isabelle/HOL. Zenodo. 2026DOI
  9. Manuel Lerchner. Voblint: Towards a Verified Goblint-Style Analysis Pipeline in Isabelle/HOL. 2026. Draftlink
  10. Xavier Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM, vol. 52, no. 7, pp. 107–115. 2009DOI
  11. Sébastien Michelland; Yannick Zakowski; Laure Gonnord. Abstract Interpreters: A Monadic Approach to Modular Verification. Proceedings of the ACM on Programming Languages, vol. 8, no. ICFP. 2024DOI
  12. Matthew Might; Panagiotis Manolios. A Posteriori Soundness for Non-deterministic Abstract Interpretations. Verification, Model Checking, and Abstract Interpretation (VMCAI 2009), vol. 5403, pp. 260–274. 2009DOI
  13. David Monniaux. Flavors of Abstract Interpretation. 2024. Lecture slides, HAL hal-04750222. Invited tutorial, European Joint Conferences on Theory and Practice of Software (ETAPS 2024), Luxembourglink
  14. Tobias Nipkow. Abstract Interpretation of Annotated Commands. Interactive Theorem Proving (ITP 2012), pp. 116–132. 2012DOI
  15. Tobias Nipkow; Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer. 2014DOI
  16. Thomas Reps; Susan Horwitz; Mooly Sagiv. Precise Interprocedural Dataflow Analysis via Graph Reachability. Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 49–61. 1995DOI
  17. Xavier Rival; Laurent Mauborgne. The Trace Partitioning Abstract Domain. ACM Transactions on Programming Languages and Systems, vol. 29, no. 5. 2007DOI
  18. Michael Schwarz. Congruences: Make % Sound by Restricting Cases Where We Return a Constant. 2023. Pull request 1161link
  19. Michael Schwarz; Simmo Saan; Helmut Seidl; Kalmer Apinis; Julian Erhard; Vesal Vojdani. Improving Thread-Modular Abstract Interpretation. Static Analysis, vol. 12913, pp. 359–383. 2021DOI
  20. Michael Schwarz; Simmo Saan; Helmut Seidl; Julian Erhard; Vesal Vojdani. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. Programming Languages and Systems (ESOP 2023), vol. 13990, pp. 28–58. 2023DOI
  21. Helmut Seidl; Varmo Vene; Markus Müller-Olm. Global Invariants for Analysing Multi-threaded Applications. Proceedings of the Estonian Academy of Sciences. Physics. Mathematics, vol. 52, no. 4, pp. 413–436. 2003DOI
  22. Helmut Seidl; Vesal Vojdani; Julian Erhard; Michael Schwarz. Mixed Flow-Sensitive Static Analysis: Engineering Modularity. FM 2026: Formal Methods, pp. 446–470. 2026DOI
  23. Micha Sharir; Amir Pnueli. Two Approaches to Interprocedural Data Flow Analysis. Program Flow Analysis: Theory and Applications. 1981
  24. Yannick Stade; Sarah Tilscher; Helmut Seidl. The Top-Down Solver Verified: Building Confidence in Static Analyzers. Computer Aided Verification, pp. 303–324. 2024. Formalization: Archive of Formal Proofs entry Top_Down_Solver, https://isa-afp.org/entries/Top_Down_Solver.htmlDOI
  25. Sarah Tilscher; Alexandra Graß; Helmut Seidl. Verifying a Solver for Mixed Flow-Sensitive Analyses. NASA Formal Methods (NFM 2026), pp. 48–69. 2026DOI
  26. Sarah Tilscher; Alexandra Graß; Helmut Seidl. Verifying a Solver for Mixed Flow-Sensitive Analyses (Artifact). Zenodo. 2026DOI
  27. Sarah Tilscher; Alexandra Graß; Helmut Seidl; Yannick Stade. Proving Total Correctness of Top-Down Solvers with Widening and Narrowing. Journal of Automated Reasoning, vol. 70, no. 2. 2026. Article 15DOI
  28. Vesal Vojdani; Kalmer Apinis; Vootele Rõtov; Helmut Seidl; Varmo Vene; Ralf Vogler. Static Race Detection for Device Drivers: The Goblint Approach. Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 391–402. 2016DOI
  29. Daniel Wasserrab. Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer. Archive of Formal Proofs. 2009link

Version history

  1. v1 · 18 pagesSubmitted by Manuel LerchnerInitial depositCurrentNov 05, 2026