Cooperative Verification: Towards Reliable Safety-Critical Systems
summary
Field has 76 distinct Java/C verifiers and more than 40 entrants in recent competitions, so the proposal is to treat verification engines as composable libraries and exchange concrete artifacts instead of reimplementing techniques. Examples: use a witness validator to cheaply check proofs, build a conditional verifier by reducing verified paths to a residual C program, and run a parallel portfolio that doubles solved industrial cases (≈140). CoVeriTeam bundles these glue components and loop‑abstraction transformers to reuse off‑the‑shelf tools.
AI-written summary · about
chapters (23)
- 0:00Intro
- 0:39Automatic Software Verification
- 2:06Competitions in Software Verification and Testing
- 4:23Different Techniques
- 7:14Cooperative Verification - Think big!
- 8:56Approaches for Combinations
- 11:36Graphical Visualization of the Coop Framework
- 13:27Definition of Cooperative Verification
- 15:24Software Verification with Witnesses
- 17:00Witness Validation
- 20:10Example Combination in DSL CoVeriTeam
- 21:59Simple Combination without Cooperation
- 23:29Facing Hard Verification Tasks
- 24:08Conditional Model Checking
- 25:55Reducer-Based Construction
- 30:32Modularization of CEGAR
- 31:03Workflow of modular CEGAR
- 35:10Interactive and Automatic Methods
- 37:50From Components: Construct Interactive Verifiers
- 39:47Component Framework: Constructing Validators
- 42:26Example: Havoc Abstraction
- 43:13Configurable Solution a la CPACHECKER
- 45:00Conclusion
related talks
01h 04mCoq's vibrant ecosystem for verification engineering
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
30mTrustworthy Runtime Verification via Bisimulation
07mV for Verification
06mFormal Verification with the Certora Prover
01h 04mSoftware Verification meets Real-World Cryptography
01h 25mIntroduction to Verifiable Computing
34mFrom Vibe Coding to Vericoding