MRPHS: Enabling Transaction-level Deductive Formal Verification Through PDVL
summary
Claims a new language PDVL enables reusable, aspect-oriented transaction-level deductive verification by compiling transactions into Gallina so proofs run in Rocq (Coq); provides open-source PDVL spec, MRPHS compiler and examples on GitHub; demonstrates a RISC‑V executable spec, calendar deadlock checks, sequential equivalence and synthesizable SystemVerilog generation; argues tactic-driven proofs scale to memory consistency and cache coherence where SMT assertion methods struggle; DATE 2024 paper and repos back the implementation.
AI-written summary · about
chapters (13)
- 0:00MRPHS and PDVL intro
- 1:27Transaction-level in PDVL
- 2:55Executable specs in PDVL
- 4:44MROR compiler integration
- 5:05Deductive verification basics
- 7:39Tactics in verification
- 8:42Equivalence checking with PDVL
- 9:44Verification papers and examples
- 10:49Comparison with other projects
- 13:21PDVL features and future
- 14:48Q&A: Modular verification
- 16:00Q&A: State relationships
- 18:54Q&A wrap-up
related talks
19mAutomated Verification of Fundamental Algebraic Laws
29mA Temporal Differential Dynamic Logic Formal Embedding
19mVelvet: A Multi-Modal Verifier for Effectful Programs
24mStrong Formal Verification For RISC V: From Instruction Set Manual To RTL
23mVerified Code Generation for the Polyhedral Model
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
46mRefinement Types from Light to Deep Verification