Preservation of Proof Obligations from Java to the Java Virtual Machine
From MaRDI portal
Publication:3541689
DOI10.1007/978-3-540-71070-7_7zbMath1165.68398OpenAlexW1891086641MaRDI QIDQ3541689
Benjamin Grégoire, Gilles Barthe, Mariela Pavlova
Publication date: 27 November 2008
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_7
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (1)
Cites Work
- A compositional natural semantics and Hoare logic for low-level languages
- Isabelle/HOL. A proof assistant for higher-order logic
- Symbolic transfer function-based approaches to certified compilation
- Certificate Translation for Optimizing Compilers
- Formal certification of a compiler back-end or
- Certificate Translation in Abstract Interpretation
This page was built for publication: Preservation of Proof Obligations from Java to the Java Virtual Machine