A Proof Assistant for Symbolic Model-Checking
Abstract elided by the publisher.
Related papers
- Live Verification in an Interactive Proof Assistant PLDI 2024
- Symbolic Automata: Omega-Regularity Modulo Theories POPL 2025
- McTT: A Verified Kernel for a Proof Assistant ICFP 2025
- Sound Borrow-Checking for Rust via Symbolic Semantics ICFP 2024
- A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson ECOOP 2024
- Static and user-extensible proof checking POPL 2012
- Automated lemma synthesis in symbolic-heap separation logic POPL 2018
- Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting CPP 2022