Certifying Temporal Properties for Compiled C Programs
Abstract elided by the publisher.
Related papers
- Establishing Local Temporal Heap Safety Properties with Applications to Compile-Time Memory Management SAS 2003
- A type system for certified binaries POPL 2002
- Cogent: uniqueness types and certifying compilation JFP 2021
- A type system for certified binaries TOPLAS 2005
- A Type System for Expressive Security Policies POPL 2000
- T2: Temporal Property Verification TACAS 2016
- Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines CPP 2019
- Leapfrog: certified equivalence for protocol parsers PLDI 2022