A Two-Level Formal Verification Methodology using HOL and COSMOS
Abstract elided by the publisher.
Related papers
- Formal verification of a concurrent bounded queue in a weak memory model ICFP 2021
- Towards verifying ethereum smart contract bytecode in Isabelle/HOL CPP 2018
- Types, bytes, and separation logic POPL 2007
- Cosmo: a concurrent separation logic for multicore OCaml ICFP 2020
- Formally Verifying a Transformation from MLTL Formulas to Regular Expressions TACAS 2025
- Complx: a verification framework for concurrent imperative programs CPP 2017
- Igloo: soundly linking compositional refinement and separation logic for distributed system verification OOPSLA 2020
- Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk) CPP 2019