Isabelle/Voblint sessions

The Congruence domain: normalized residue-class lattice, arithmetic, backward filtering, transfers, executable bridge

The int_dom analysis family: a reduced product of Sign, Interval, Parity and Congruence, with verified progressive and structural-fixpoint refinement

The Interval domain: bounds, lattice, widening, executable bridge, end-to-end soundness

The Parity domain: lattice, transfers, executable bridge

Order carriers that are not pointwise abstract states

The Sign domain: seven-element lattice, executable bridge, end-to-end soundness

Procedure-aware CFG: the graph model and its activation-trace semantics

Production CLI-facing surface: run_voblint over the six analyses, every
     global update rule and every context policy, with its soundness theorems,
     independent of the demonstration and regression theories in
     Voblint_Examples

Code export boundary for the Voblint CLI and GraphViz surfaces

VIMP-to-CFG compiler, its structural invariants, and forward simulation

Abstract value domains, pointwise states, and reachability constructions

The project capstone: a fully discharged end-to-end certificate and the
     narrative index that imports every example session

Domain-independent compiler witness: the call-free compilation theorem every
     domain's flagship run reuses, plus regression assertions pinning VIMP
     concrete syntax, precedence, expression semantics and compiled edges

Witnesses that reach the CLI layer: a domain's codegen entry point or the
     public run_voblint operation.  They see every
     domain because Voblint_CLI does, which is why they are not in the per-domain
     example sessions

Congruence: the end-to-end D/G witness

int_dom: a certified run of the reduced product under each refinement mode

Interval witnesses: the flagship certified runs and entry-value contexts
     (under Ctx/)

Parity witnesses: the flagship certified run

A carrier that is not a pointwise abstract state, run through the same
     generator: the relational demo, over interval bounds

Sign witnesses: a certified run and call-string contexts

Solver- and generator-layer witnesses, stated over whichever domain makes the
     effect visible rather than to demonstrate that domain

Executable carrier and transport: the solver runs on association lists, soundness is stated over functions

The D/G analysis framework: transfer contract, equation generator, and collecting soundness

What a non-relational domain reuses: expression evaluation and soundness,
     special-call dispatch, generic procedure entry and executable backward filtering.
     Every theory here fixes an abstract state as one value per variable,
     which is why a relational carrier must not be able to reach it

The output end: what a solved routed system publishes, and the surface a
     caller reads it through

Shared equation construction and concrete context policies over
     compiled programs, including key-space finiteness arguments

The strategy-tree equation language of the vendored side-effecting solver

VIMP syntax, small-step, and procedure language