RPP: Automatic Proof of Relational Properties by Self-composition
Abstract elided by the publisher.
Related papers
- Property Directed Self Composition CAV 2019
- Merging Inductive Relations PLDI 2023
- Verifying Hyperliveness CAV 2019
- Lazy Self-composition for Security Verification CAV 2018
- A vision of miking: interactive programmatic modeling, sound language composition, and self-learning compilation SLE 2019
- Decomposition instead of self-composition for proving the absence of timing channels PLDI 2017
- Proving hypersafety compositionally OOPSLA 2022
- Compositional Verification of Heap-Manipulating Programs Through Property-Guided Learning APLAS 2019