The Rely-Guarantee Method in Isabelle/HOL
Abstract elided by the publisher.
Related papers
- A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL CPP 2015
- Safety and conservativity of definitions in HOL and Isabelle/HOL POPL 2018
- An Isabelle/HOL formalization of AProVE's termination method for LLVM IR CPP 2021
- The Poincaré-Bendixson theorem in Isabelle/HOL CPP 2020
- Encoding Dependently-Typed Constructions into Simple Type Theory CPP 2023
- Verifying the CPS Transformation in Isabelle/HOL APLAS 2001
- Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory CPP 2013
- Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL TACAS 1999