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

VerificationAssume-guarantee reasoningAutomated theorem provingConcurrent softwareSoftware engineeringVerification 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

• 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?)
• Avoiding exponential explosion: generating compact verification conditions
• Compositional action system refinement
• Guarded commands, nondeterminacy and formal derivation of programs
• 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
• Model checking of concurrent algorithms: from Java to C
• SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs
• Verification of parameterized concurrent programs by modular reasoning about data and control
• Atomizer: a dynamic atomicity checker for multithreaded programs
• A mechanism of function calls in MSVL
• Context-Sensitive Multivariant Assertion Checking in Modular Programs
• scientific article; zbMATH DE number 2087551 (Why is no real title available?)
• Underspecified harnesses and interleaved bugs
• A Basis for Verifying Multi-threaded Programs
• Atomizer: A dynamic atomicity checker for multithreaded programs
• scientific article; zbMATH DE number 1670568 (Why is no real title available?)
• scientific article; zbMATH DE number 1903353 (Why is no real title available?)
• scientific article; zbMATH DE number 1701757 (Why is no real title available?)
• Towards Efficient Verification of Systems with Dynamic Process Creation
• Compositional reasoning
• Cloud-based verification of concurrent software

Describes a project that uses

Uses Software

• SIMPLIFY
• ESC/Java
• Mercator

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)