Verifying Invariants Using theorem Proving
No abstract available.
Related papers
- Synthesizing Implication Lemmas for Interactive Theorem Proving OOPSLA 2025
- GACAL: Conjecture-Based Verification - (Competition Contribution) TACAS 2020
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System VMCAI 2007
- Combining Model Checking and Theorem Proving to Verify Parallel Processes CAV 1993
- Verifying the SRT Division Algorithm Using Theorem Proving Techniques CAV 1996
- Overcoming restraint: composing verification of foreign functions with cogent CPP 2022
- Connecting Higher-Order Separation Logic to a First-Order Outside World ESOP 2020
- ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference - (Competition Contribution) TACAS 2019