Verifying the CPS Transformation in Isabelle/HOL
No abstract available.
Related papers
- VeriPhy: verified controller executables from verified cyber-physical system models PLDI 2018
- Verifying Term Graph Optimizations using Isabelle/HOL CPP 2023
- Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL TACAS 1999
- An Isabelle/HOL formalization of AProVE's termination method for LLVM IR CPP 2021
- A Verified Compiler from Isabelle/HOL to CakeML ESOP 2018
- A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL CPP 2019
- Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem CPP 2019
- Towards verifying ethereum smart contract bytecode in Isabelle/HOL CPP 2018