Modular verification of multithreaded programs
From MaRDI portal
Publication:557795
DOI10.1016/j.tcs.2004.12.006zbMath1108.68080OpenAlexW2112381327MaRDI QIDQ557795
Sanjit A. Seshia, Cormac Flanagan, Shaz Qadeer, Stephen N. Freund
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
Software engineeringVerificationAssume-guarantee reasoningAutomated theorem provingConcurrent softwareVerification conditions
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (4)
Compositional Reasoning ⋮ A mechanism of function calls in MSVL ⋮ Local proofs for global safety properties ⋮ Towards Efficient Verification of Systems with Dynamic Process Creation
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Compositional action system refinement
- P-A logic - a compositional proof system for distributed programs
- Verification: Theory and practice. Essays dedicated to Zohar Manna on the occasion of his 64th birthday.
- Simplify: a theorem prover for program checking
- Specifying Concurrent Program Modules
- Tentative steps toward a development method for interfering programs
- Proofs of Networks of Processes
- Guarded commands, nondeterminacy and formal derivation of programs
- Reduction
- Logical foundations for compositional verification and development of concurrent programs in UNITY
- Verifying safety properties of concurrent Java programs using 3-valued logic
- Avoiding exponential explosion
- Formal Methods for Open Object-Based Distributed Systems
This page was built for publication: Modular verification of multithreaded programs
