An assertion-based proof system for multithreaded Java

DOI10.1016/j.tcs.2004.09.019zbMath1070.68016OpenAlexW2140426285MaRDI QIDQ1770359

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

Publication date: 6 April 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/14587

zbMATH Keywords

Javarelative completenessVerificationSoundnessMultithreadingHoare-logicMonitors

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Related Items (9)

MAVEN: Modular aspect verification and interference analysis ⋮ A system for compositional verification of asynchronous objects ⋮ A dynamic logic for deductive verification of multi-threaded programs ⋮ A program logic for resources ⋮ A Bibliography of Willem-Paul de Roever ⋮ A Proof System for a PGAS Language ⋮ Fifty years of Hoare's logic ⋮ A shared-variable concurrency analysis of multi-threaded object-oriented programs ⋮ Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects

Uses Software

• PVS
• JML

Cites Work

• A proof technique for communicating sequential processes
• An axiomatic proof technique for parallel programs
• How the design of JML accommodates both runtime assertion checking and formal verification
• Specification and verification of object-oriented programs using supertype abstraction
• A Proof System for Communicating Sequential Processes
• Hoare logic for Java in Isabelle/HOL
• An axiomatic basis for computer programming
• Formal Methods for Components and Objects
• Formal Methods for Open Object-Based Distributed Systems
• Formal Methods for Open Object-Based Distributed Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: An assertion-based proof system for multithreaded Java