Automated Certification of Implicit Induction Proofs
No abstract available.
Related papers
- Self-certification: bootstrapping certified typecheckers in F* with Coq POPL 2012
- CycleQ: an efficient basis for cyclic equational reasoning PLDI 2022
- Progress in Certifying Hardware Model Checking Results CAV 2021
- Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models TACAS 2021
- Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper) CPP 2018
- Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems CAV 2019
- Separation Logic with Monadic Inductive Definitions and Implicit Existentials APLAS 2015
- Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays ESOP 2010