A compositional natural semantics and Hoare logic for low-level languages

DOI10.1016/j.tcs.2006.12.020zbMath1111.68071OpenAlexW2170606418MaRDI QIDQ877026

Ando Saabas, Tarmo Uustalu

Publication date: 19 April 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.12.020

zbMATH Keywords

compositionalitynatural semanticslow-level languagescompilation of proofsHoare logics

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

Proof optimization for partial redundancy elimination ⋮ Certifying assembly with formal security proofs: the case of BBS ⋮ Equational Theories of Abnormal Termination Based on Kleene Algebra ⋮ Preservation of Proof Obligations from Java to the Java Virtual Machine ⋮ Program and proof optimizations with type systems ⋮ Relational bytecode correlations

Cites Work

• Unnamed Item
• Unnamed Item
• Program and proof optimizations with type systems
• Goto statements: Semantics and deduction systems
• Axiomatic approach to side effects and general jumps
• Theorem proving in higher order logics. 16th international conference, TPHOLs 2003, Rome, Italy, September 8--12, 2003. Proceedings
• Program proving: KJumps and functions
• A critique of the foundations of Hoare style programming logics
• Soundness and Completeness of an Axiom System for Program Verification
• Certified assembly programming with embedded code pointers
• Programming Languages and Systems
• An axiomatic basis for computer programming
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: A compositional natural semantics and Hoare logic for low-level languages