Modular verification of multithreaded programs

DOI10.1016/J.TCS.2004.12.006MaRDI QIDQ557795zbMATH OpenOpenAlexFDO

Authors Cormac Flanagan, Stephen N. Freund, Shaz Qadeer, Sanjit A. Seshia

Publication date 30 June 2005

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

Full work available at URL https://escholarship.org/uc/item/9753d15c

zbMATH Keywords

Assume-guarantee reasoningAutomated theorem provingConcurrent softwareSoftware engineeringVerificationVerification conditions

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• scientific article; zbMATH DE number 1903353
• scientific article; zbMATH DE number 2087551
• Atomizer: A dynamic atomicity checker for multithreaded programs
• Model checking of concurrent algorithms: from Java to C
• A Basis for Verifying Multi-threaded Programs

Cites work

• Avoiding exponential explosion: generating compact verification conditions
• Compositional action system refinement
• Guarded commands, nondeterminacy and formal derivation of programs
• scientific article; zbMATH DE number 1670562 (Why is no real title available?)
• scientific article; zbMATH DE number 1701757 (Why is no real title available?)
• scientific article; zbMATH DE number 986404 (Why is no real title available?)
• scientific article; zbMATH DE number 3938541 (Why is no real title available?)
• scientific article; zbMATH DE number 4050933 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 2087551 (Why is no real title available?)
• scientific article; zbMATH DE number 1903353 (Why is no real title available?)
• Inductive proof outlines for monitors in Java.
• Logical foundations for compositional verification and development of concurrent programs in UNITY
• P-A logic - a compositional proof system for distributed programs
• Proofs of Networks of Processes
• Reduction
• Simplify: a theorem prover for program checking
• Specifying Concurrent Program Modules
• Tentative steps toward a development method for interfering programs
• Verification: Theory and practice. Essays dedicated to Zohar Manna on the occasion of his 64th birthday.
• Verifying safety properties of concurrent Java programs using 3-valued logic

Cited in

(17)

• Local proofs for global safety properties
• scientific article; zbMATH DE number 1670568 (Why is no real title available?)
• scientific article; zbMATH DE number 1701757 (Why is no real title available?)
• Cloud-based verification of concurrent software
• Underspecified harnesses and interleaved bugs
• Verification of parameterized concurrent programs by modular reasoning about data and control
• Model checking of concurrent algorithms: from Java to C
• Compositional reasoning
• A mechanism of function calls in MSVL
• Atomizer: a dynamic atomicity checker for multithreaded programs
• A Basis for Verifying Multi-threaded Programs
• SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs
• scientific article; zbMATH DE number 2087551 (Why is no real title available?)
• scientific article; zbMATH DE number 1903353 (Why is no real title available?)
• Context-Sensitive Multivariant Assertion Checking in Modular Programs
• Towards Efficient Verification of Systems with Dynamic Process Creation
• Atomizer: A dynamic atomicity checker for multithreaded programs

Describes a project that uses

Uses Software

• ESC/Java
• Mercator
• SIMPLIFY

This page was built for publication: Modular verification of multithreaded programs

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