Mechanising a type-safe model of multithreaded Java with a verified compiler
type: Item
instance of: scholarly article
title: Mechanising a type-safe model of multithreaded Java with a verified compiler
zbMATH Open document ID: 1451.68178
author: Andreas Lochbihler
published in: Journal of Automated Reasoning
publication date: 2018-08-21T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N15
Mathematics Subject Classification ID: 68N20
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 6921417
zbMATH Keywords: Java
zbMATH Keywords: concurrency
zbMATH Keywords: type safety
zbMATH Keywords: compiler verification
zbMATH Keywords: operational semantics
Wikidata QID: Q123135102
describes a project that uses: CakeML
describes a project that uses: Locales
describes a project that uses: Archive Formal Proofs
describes a project that uses: Jinja not Java
describes a project that uses: CLDC
describes a project that uses: Isabelle/HOL
describes a project that uses: JavaFAN
describes a project that uses: Cyclone
describes a project that uses: K Prover
describes a project that uses: Nitpick
describes a project that uses: CompCertTSO
describes a project that uses: K-Java
describes a project that uses: Jinja Threads
describes a project that uses: BicolanoMT
MaRDI profile type: Publication
full work available at URL: s10817-018-9452-x
OpenAlex ID: W2790469097
cites work: Axiomatizing prefix iteration with silent steps
cites work: A syntactic approach to type soundness
cites work: Locales: a module system for mathematical theories
cites work: Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
cites work: CompCertTSO
cites work: Computer Aided Verification
cites work: An overview of the K semantic framework
cites work: Q4068060
cites work: Verified lightweight bytecode verification
cites work: Verified bytecode verifiers.
cites work: Verified bytecode verification and type-certifying compilation
cites work: Verified bytecode subroutines
cites work: CakeML
cites work: How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
cites work: Formal certification of a compiler back-end or
cites work: A formally verified compiler back-end
cites work: Formal verification of a C-like memory model and its uses for verifying program transformations
cites work: Theorem Proving in Higher Order Logics
cites work: Verifying a Compiler for Java Threads
cites work: Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
cites work: Animating the Formalised Semantics of a Java-Like Language
cites work: Q3929062
cites work: Q3992568
cites work: From Jinja bytecode to term rewriting: a complexity reflecting transformation
cites work: Q2769440
cites work: \(\mu\)Java: Embedding a programming language in a theorem prover
cites work: Hoare logic for Java in Isabelle/HOL
cites work: Q4808824
cites work: Formal verification of object layout for c++ multiple inheritance
cites work: Logic for Programming, Artificial Intelligence, and Reasoning
cites work: Q2742791
cites work: Q4809043
cites work: Q4428314
DOI: 10.1007/S10817-018-9452-X
Recommended article: Q4472236
Recommended article: An assertion-based proof system for multithreaded Java
Recommended article: Q5447372
Recommended article: Verifying a Compiler for Java Threads
Recommended article: Q2753763
Recommended article: Q2722012
Recommended article: Formal Methods for Components and Objects
Recommended article: Q5457270
description: scientific article; zbMATH DE number 6921417