Verifying a Local Generic Solver in Coq
Abstract elided by the publisher.
Related papers
- Spy game: verifying a local generic solver in Iris POPL 2020
- Practical Tactics for Verifying C Programs in Coq CPP 2015
- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver CAV 2021
- A Formalization of Core Why3 in Coq POPL 2024
- Formal Verification of WTO-based Dataflow Solvers ESOP 2025
- Seam: provably safe local edits on graphs OOPSLA 2017
- Accelerating Automated Program Verifiers by Automatic Proof Localization CAV 2025
- Certifying graph-manipulating C programs via localizations within data structures OOPSLA 2019