Mechanising a type-safe model of multithreaded Java with a verified compiler
DOI10.1007/S10817-018-9452-XzbMATH Open1451.68178OpenAlexW2790469097WikidataQ123135102 ScholiaQ123135102MaRDI QIDQ1663233FDOQ1663233
Publication date: 21 August 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-018-9452-x
Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Computer Aided Verification
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- CompCertTSO
- An overview of the K semantic framework
- Title not available (Why is that?)
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Locales: a module system for mathematical theories
- Title not available (Why is that?)
- CakeML
- Title not available (Why is that?)
- Animating the Formalised Semantics of a Java-Like Language
- A syntactic approach to type soundness
- Hoare logic for Java in Isabelle/HOL
- Formal certification of a compiler back-end or
- Theorem Proving in Higher Order Logics
- A formally verified compiler back-end
- Title not available (Why is that?)
- Verified bytecode verification and type-certifying compilation
- Title not available (Why is that?)
- Logic for Programming, Artificial Intelligence, and Reasoning
- Title not available (Why is that?)
- Verifying a Compiler for Java Threads
- Verified bytecode verifiers.
- Verified bytecode subroutines
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Axiomatizing prefix iteration with silent steps
- Title not available (Why is that?)
- Verified lightweight bytecode verification
- From Jinja bytecode to term rewriting: a complexity reflecting transformation
- \(\mu\)Java: Embedding a programming language in a theorem prover
- Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
- Title not available (Why is that?)
- Formal verification of object layout for c++ multiple inheritance
Cited In (9)
- Title not available (Why is that?)
- Verifying a Compiler for Java Threads
- A safe variant of the unsafe integer arithmetic of Java™
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A formal semantics of the GraalVM intermediate representation
- Title not available (Why is that?)
- Type safety in the JVM: some problems in Java 2 SDK 1.2 and proposed solutions
Uses Software
Recommendations
- Title not available (Why is that?) 👍 👎
- An assertion-based proof system for multithreaded Java 👍 👎
- A verifying compiler for a multi-threaded object-oriented language 👍 👎
- Verifying a Compiler for Java Threads 👍 👎
- Title not available (Why is that?) 👍 👎
- Title not available (Why is that?) 👍 👎
- A tool-supported proof system for multithreaded Java. 👍 👎
- A deductive proof system for multithreaded Java with exceptions 👍 👎
This page was built for publication: Mechanising a type-safe model of multithreaded Java with a verified compiler
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663233)
