Towards a machine-checked Java specification book

DOI10.1007/3-540-44659-1_30MaRDI QIDQ2754065zbMATH OpenFDO

Authors Bernhard Reus, Tatjana Hein

Publication date 18 December 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44659-1_30

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Java and the Java memory model -- a unified, machine-checked formalisation
• A unified formal specification and analysis of the new Java memory models
• scientific article; zbMATH DE number 2090288
• A tool-supported proof system for multithreaded Java.
• The Java Memory Model: Operationally, Denotationally, Axiomatically

Cited in

(8)

• K-Java: a complete semantics of Java
• Java and the Java memory model -- a unified, machine-checked formalisation
• Animating the formalised semantics of a Java-like language
• Formal modelling of Java GUI event handling
• Formal reasoning about hardware and software memory models
• Algebraic Methodology and Software Technology
• Theorem Proving in Higher Order Logics
• ZB 2005: Formal Specification and Development in Z and B

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL

This page was built for publication: Towards a machine-checked Java specification book

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