Animating the Formalised Semantics of a Java-Like Language

DOI10.1007/978-3-642-22863-6_17zbMath1342.68294MaRDI QIDQ3088008

Andreas Lochbihler, Lukas Bulwahn

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

68N15: Theory of programming languages

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL, Mechanising a type-safe model of multithreaded Java with a verified compiler

Uses Software

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

Cites Work

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