A deductive proof system for multithreaded Java with exceptions

MaRDI QIDQ5457270zbMATH OpenFDO

Authors Erika Ábrahám, Martin Steffen, Frank S. de Boer, Willem-Paul de Roever

Publication date 14 April 2008

zbMATH Keywords

assertional proof methodconcurrencyexception handling

Mathematics Subject Classification ID

Logic in computer science (03B70) 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

• An assertion-based proof system for multithreaded Java
• A tool-supported proof system for multithreaded Java.
• scientific article; zbMATH DE number 1759614
• A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs
• scientific article; zbMATH DE number 2087419

Cited in

(12)

• Mechanising a type-safe model of multithreaded Java with a verified compiler
• An assertion-based proof system for multithreaded Java
• scientific article; zbMATH DE number 1692946 (Why is no real title available?)
• Safe locking for multi-threaded Java with exceptions
• scientific article; zbMATH DE number 1759614 (Why is no real title available?)
• A compositional operational semantics for Java\(_{\text{MT}}\)
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs
• A tool-supported proof system for multithreaded Java.
• Inductive proof outlines for monitors in Java.
• An operational semantics for object-oriented concepts based on the class hierarchy
• Proof theory for exception handling in a tasking environment

Describes a project that uses

Uses Software

• PVS
• JML

This page was built for publication: A deductive proof system for multithreaded Java with exceptions

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