Deriving correctness properties of compiled code

DOI10.1007/BF01383985zbMath0785.68061OpenAlexW2996838589MaRDI QIDQ1309251

Paul Curzon

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

zbMATH Keywords

compiler correctnessprogramming logicHOL systemmachine-checked formal verificationobject code correctness

Mathematics Subject Classification ID

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

• IBM PC Assembler

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