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.
Formal Aspects of Computing27(3), 573–609 (2015)
8 Pith papers cite this work. Polarity classification is still indexing.
8
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
roles
background 1polarities
background 1representative citing papers
CNnotator shows LLMs can synthesize CN specifications for memory usage in small-to-medium C programs, reaching 97% success with reasoning models.
Caesar introduces a deductive verifier for probabilistic programs using the HeyVL language, Z3 SMT solving, and a probabilistic model-checking backend after five years of development.
LeetProof achieves higher rates of fully certified program synthesis from natural language by using a multi-modal verifier in Lean to validate specifications via randomized testing and delegate proofs to AI tools, outperforming single-mode baselines on benchmarks while uncovering defects in prior参考.
Analysis of 4,913 C projects found 37% use at least one GCC builtin, 10 builtins cover over 30% of projects, 110 cover 90%, builtins are still being added, and many tools have incomplete or incorrect support.
The authors define general non-functional rules for C modules, propose an interface contract language, implement a Frama-C checker plugin, and demonstrate verification on two Scania truck codebases alongside ACSL functional contracts.
AutoRocq is an LLM agent that learns proofs on-the-fly by collaborating with the Rocq prover to verify programs on SV-COMP benchmarks and Linux kernel modules.
QCP combines automatic separation logic verification with Rocq interactive proving for C programs via annotations and a VS Code extension.
citing papers explorer
-
CNnotator: LLM-Guided Memory Safety Annotation Synthesis
CNnotator shows LLMs can synthesize CN specifications for memory usage in small-to-medium C programs, reaching 97% success with reasoning models.
-
Caesar: A Deductive Verifier for Probabilistic Programs
Caesar introduces a deductive verifier for probabilistic programs using the HeyVL language, Z3 SMT solving, and a probabilistic model-checking backend after five years of development.
-
Understanding GCC Builtins to Develop Better Tools
Analysis of 4,913 C projects found 37% use at least one GCC builtin, 10 builtins cover over 30% of projects, 110 cover 90%, builtins are still being added, and many tools have incomplete or incorrect support.
-
Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code
The authors define general non-functional rules for C modules, propose an interface contract language, implement a Frama-C checker plugin, and demonstrate verification on two Scania truck codebases alongside ACSL functional contracts.
-
QCP: A Practical Separation Logic-based C Program Verification Tool
QCP combines automatic separation logic verification with Rocq interactive proving for C programs via annotations and a VS Code extension.