Mechanising a type-safe model of multithreaded Java with a verified compiler
From MaRDI portal
(Redirected from Publication:1663233)
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)
Recommendations
- scientific article; zbMATH DE number 2080048
- An assertion-based proof system for multithreaded Java
- A verifying compiler for a multi-threaded object-oriented language
- Verifying a Compiler for Java Threads
- scientific article; zbMATH DE number 1670562
- scientific article; zbMATH DE number 1617288
- A tool-supported proof system for multithreaded Java.
- A deductive proof system for multithreaded Java with exceptions
Cites work
- scientific article; zbMATH DE number 1650458 (Why is no real title available?)
- scientific article; zbMATH DE number 1701360 (Why is no real title available?)
- scientific article; zbMATH DE number 3744561 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 3485178 (Why is no real title available?)
- scientific article; zbMATH DE number 1980940 (Why is no real title available?)
- scientific article; zbMATH DE number 2090132 (Why is no real title available?)
- scientific article; zbMATH DE number 2090288 (Why is no real title available?)
- A formally verified compiler back-end
- A syntactic approach to type soundness
- An overview of the K semantic framework
- Animating the formalised semantics of a Java-like language
- Axiomatizing prefix iteration with silent steps
- CakeML
- CompCertTSO
- Computer Aided Verification
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Formal verification of object layout for C++ multiple inheritance
- From Jinja bytecode to term rewriting: a complexity reflecting transformation
- Hoare logic for Java in Isabelle/HOL
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Java and the Java memory model -- a unified, machine-checked formalisation
- Locales: a module system for mathematical theories
- Logic for Programming, Artificial Intelligence, and Reasoning
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Theorem Proving in Higher Order Logics
- Verified bytecode subroutines
- Verified bytecode verification and type-certifying compilation
- Verified bytecode verifiers.
- Verified lightweight bytecode verification
- Verifying a Compiler for Java Threads
- \(\mu\)Java: Embedding a programming language in a theorem prover
Cited in
(12)- scientific article; zbMATH DE number 7649976 (Why is no real title available?)
- Verifying a Compiler for Java Threads
- A safe variant of the unsafe integer arithmetic of Java™
- scientific article; zbMATH DE number 2089402 (Why is no real title available?)
- scientific article; zbMATH DE number 1617288 (Why is no real title available?)
- scientific article; zbMATH DE number 1670562 (Why is no real title available?)
- Jinja: towards a comprehensive formal semantics for a Java-like language
- A formal semantics of the GraalVM intermediate representation
- scientific article; zbMATH DE number 2090288 (Why is no real title available?)
- Type safety in the JVM: some problems in Java 2 SDK 1.2 and proposed solutions
- A Certified Data Race Analysis for a Java-like Language
- Animating the formalised semantics of a Java-like language
Describes a project that uses
Uses Software
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)
