scientific article; zbMATH DE number 1617288

zbMATH Open0966.68554MaRDI QIDQ2722012FDOQ2722012

Erik Poll, Joachim van den Berg, Bart Jacobs, Marieke Huisman

Publication date: 11 July 2001

Title of this publication is not available (Why is that?)

Recommendations

• Java and the Java memory model -- a unified, machine-checked formalisation
• Java Memory Model-Aware Model Checking
• scientific article; zbMATH DE number 1951189
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• The safety-critical Java memory model formalised
• scientific article; zbMATH DE number 5499373
• Verification of Concurrent Programs on Weak Memory Models

Mathematics Subject Classification ID

Theory of programming languages (68N15) Computing methodologies and applications (68U99) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (9)

• Title not available (Why is that?)
• Coalgebras and monads in the semantics of Java
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Weakest pre-condition reasoning for Java programs with JML annotations
• Static Analysis
• The Java Memory Model: Operationally, Denotationally, Axiomatically
• Java Memory Model-Aware Model Checking
• The safety-critical Java memory model formalised

Uses Software

• Isabelle
• Isabelle/HOL
• PVS
• JML

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2722012)