Preservation of Proof Obligations from Java to the Java Virtual Machine

DOI10.1007/978-3-540-71070-7_7MaRDI QIDQ3541689zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, Benjamin Grégoire, 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

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

Recommendations

• A Bytecode Logic for JML and Types
• scientific article; zbMATH DE number 2090288
• Certificates and Separation Logic
• Completeness of a bytecode verifier and a certifying Java-to-JVM compiler
• Theorem Proving in Higher Order Logics

Cites work

• A compositional natural semantics and Hoare logic for low-level languages
• Certificate Translation for Optimizing Compilers
• Certificate Translation in Abstract Interpretation
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Isabelle/HOL. A proof assistant for higher-order logic
• Symbolic transfer function-based approaches to certified compilation

Cited in

(2)

• CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
• Certificates and Separation Logic

This page was built for publication: Preservation of Proof Obligations from Java to the Java Virtual Machine

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3541689)