Animating the formalised semantics of a Java-like language

DOI10.1007/978-3-642-22863-6_17MaRDI QIDQ3088008zbMATH OpenOpenAlexFDO

Authors Lukas Bulwahn, Andreas Lochbihler

Publication date 17 August 2011

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-22863-6_17

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Jinja: towards a comprehensive formal semantics for a Java-like language
• scientific article; zbMATH DE number 1670761
• Verifying a Compiler for Java Threads
• scientific article; zbMATH DE number 1692947

Cites work

• A formally verified compiler back-end
• Algebraic Methodology and Software Technology
• Certification of Termination Proofs Using CeTA
• Code generation via higher-order rewrite systems
• CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
• Extraction in Coq: An Overview
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
• Imperative Functional Programming with Isabelle/HOL
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• The Isabelle collections framework
• Turning Inductive into Equational Specifications
• Verifying a Compiler for Java Threads

Cited in

(6)

• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Integrating formal specifications into applications: the ProB Java API
• From LCF to Isabelle/HOL
• Automatic refinement to efficient data structures: a comparison of two approaches
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Jinja: towards a comprehensive formal semantics for a Java-like language

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• JavaFAN
• CoqJVM
• HOL
• CeTA
• Flyspeck
• FinFuns
• Jinja Threads
• Tame Graphs
• Archive Formal Proofs

This page was built for publication: Animating the formalised semantics of a Java-like language

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