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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Locales: a module system for mathematical theories
- CakeML
- 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
- Verified bytecode verification and type-certifying compilation
- Logic for Programming, Artificial Intelligence, and Reasoning
- 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
- 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
- Formal verification of object layout for c++ multiple inheritance
Cited In (7)
- 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?)
- A formal semantics of the GraalVM intermediate representation
- 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?) 👍 👎
- Title not available (Why is that?) 👍 👎
- Title not available (Why is that?) 👍 👎
- Title not available (Why is that?) 👍 👎
- Title not available (Why is that?) 👍 👎
- An assertion-based proof system for multithreaded Java 👍 👎
- Verifying a Compiler for Java Threads 👍 👎
- Formal Methods for Components and Objects 👍 👎
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)
