Deriving correctness properties of compiled code
From MaRDI portal
Publication:1309251
DOI10.1007/BF01383985zbMath0785.68061OpenAlexW2996838589MaRDI QIDQ1309251
Publication date: 3 May 1994
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf01383985
compiler correctnessprogramming logicHOL systemmachine-checked formal verificationobject code correctness
Theory of compilers and interpreters (68N20) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Specification, verification and prototyping of an optimized compiler ⋮ A Completely Verified Realistic Bootstrap Compiler
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- A demonstrably correct compiler
- The notion of proof in hardware verification
- Compiler specification and verification
- Mechanizing some advanced refinement concepts
- An axiomatic definition of the programming language Pascal
- The use of ghost variables and virtual programming in the documentation and verification of programs
- An axiomatic basis for computer programming