cs.LO — Logic in Computer Science
Voblint: End-to-End Soundness of a Context-Sensitive Goblint-Style Analyzer in Isabelle/HOL
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.