Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving
Abstract elided by the publisher.
Related papers
- Show Me The Money: An Exercise in Proof-Driven Software Understanding CAV 2026
- Connecting Higher-Order Separation Logic to a First-Order Outside World ESOP 2020
- Formal Verification of Quantum Ancilla Safety CAV 2026
- Combining Model Checking and Theorem Proving to Verify Parallel Processes CAV 1993
- An order-aware dataflow model for parallel Unix pipelines ICFP 2021
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System VMCAI 2007
- Compositional optimizations for CertiCoq ICFP 2021
- Passport: Improving Automated Formal Verification Using Identifiers TOPLAS 2023