Modular verification of multithreaded programs

DOI10.1016/J.TCS.2004.12.006zbMATH Open1108.68080OpenAlexW2112381327MaRDI QIDQ557795FDOQ557795

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

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

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)

Cites Work

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

Cited In (17)

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

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)