Animating the Formalised Semantics of a Java-Like Language
From MaRDI portal
Publication:3088008
DOI10.1007/978-3-642-22863-6_17zbMath1342.68294MaRDI QIDQ3088008
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
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, From LCF to Isabelle/HOL, Automatic refinement to efficient data structures: a comparison of two approaches
Uses Software
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