Formal verification of a Java compiler in Isabelle
From MaRDI portal
Recommendations
Cited in
(28)- Mechanising a type-safe model of multithreaded Java with a verified compiler
- Verified bytecode verification and type-certifying compilation
- Safe functional systems through integrity types and verified assembly
- A verified compiler from Isabelle/HOL to CakeML
- A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
- Formal verification of a compiler back-end generic checker program
- Java: Embedding a programming language in a theorem prover
- Towards a machine-checked Java specification book
- A Hoare calculus for verifying Java realizations of OCL-constrained design models
- The LOOP compiler for Java and JML
- A formal framework for Java separate compilation
- Formal Certification of a Resource-Aware Language Implementation
- Automatic Parallelization and Optimization of Programs by Proof Rewriting
- CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
- Preservation of Proof Obligations from Java to the Java Virtual Machine
- Formalising and Verifying Reference Attribute Grammars in Coq
- Refinement algebra for formal bytecode generation
- Precision in practice: A type-preserving Java compiler
- Formalization and verification of a mail server in Coq
- Compiling a 50-year journey
- Formal techniques for Java programs
- Verification and code generation for invariant diagrams in Isabelle
- A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- scientific article; zbMATH DE number 5499373 (Why is no real title available?)
- Formal compiler construction in a logical framework
- A mechanical analysis of program verification strategies
This page was built for publication: Formal verification of a Java compiler in Isabelle
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4809043)
