Mechanising a type-safe model of multithreaded Java with a verified compiler

DOI10.1007/s10817-018-9452-xzbMath1451.68178OpenAlexW2790469097WikidataQ123135102 ScholiaQ123135102MaRDI QIDQ1663233

Andreas Lochbihler

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

zbMATH Keywords

operational semanticsJavaconcurrencytype safetycompiler verification

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

A formal semantics of the GraalVM intermediate representation ⋮ Unnamed Item

Uses Software

• Nitpick
• Isabelle/HOL
• JavaFAN
• CompCertTSO
• CakeML
• Cyclone
• Locales
• K-Java
• Jinja Threads
• BicolanoMT
• Archive Formal Proofs
• Jinja not Java
• CLDC
• K Prover

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formal verification of a C-like memory model and its uses for verifying program transformations
• An overview of the K semantic framework
• A syntactic approach to type soundness
• Verified bytecode subroutines
• From Jinja bytecode to term rewriting: a complexity reflecting transformation
• Verified bytecode verifiers.
• Verified bytecode verification and type-certifying compilation
• Axiomatizing prefix iteration with silent steps
• Locales: a module system for mathematical theories
• A formally verified compiler back-end
• Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
• Animating the Formalised Semantics of a Java-Like Language
• Verifying a Compiler for Java Threads
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Verified lightweight bytecode verification
• Hoare logic for Java in Isabelle/HOL
• Computer Aided Verification
• Formal certification of a compiler back-end or
• CompCertTSO
• CakeML
• Formal verification of object layout for c++ multiple inheritance
• Theorem Proving in Higher Order Logics
• Logic for Programming, Artificial Intelligence, and Reasoning
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

This page was built for publication: Mechanising a type-safe model of multithreaded Java with a verified compiler