Verifying the SRT Division Algorithm Using Theorem Proving Techniques
Abstract elided by the publisher.
Related papers
- Modular Verification of SRT Division CAV 1996
- Synthesizing Implication Lemmas for Interactive Theorem Proving OOPSLA 2025
- Reasoning About Programs POPL 1973
- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver CAV 2021
- Verifying Invariants Using theorem Proving CAV 1996
- Combining Model Checking and Theorem Proving to Verify Parallel Processes CAV 1993
- Automating Proofs of the Absence of Common Runtime Errors POPL 1978
- A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq Haskell 2017