HDL defines dynamic theories with lifting and combination operations, proves soundness and relative completeness in Isabelle, and demonstrates the approach on a Java controller steering a differential dynamic logic plant model.
Boogie: a modular reusable verifier for object-oriented programs
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
representative citing papers
Forge pipeline combines LLM code generation with MDE transformations to produce verifiable artifacts in Dafny, CSP, and Isabelle, iterating on failures to generate standards-relevant evidence for Java code.
SEMBridge uses a tagless-final interface in a Python prototype to derive executable state transformers and verification conditions from the same loop-free imperative program definitions, tested on five examples up to 729 states.
citing papers explorer
-
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
HDL defines dynamic theories with lifting and combination operations, proves soundness and relative completeness in Isabelle, and demonstrates the approach on a Java controller steering a differential dynamic logic plant model.