Preservation of Proof Obligations from Java to the Java Virtual Machine

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Certificates and Separation Logic

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