Modular verification of multithreaded programs

DOI10.1016/j.tcs.2004.12.006zbMath1108.68080MaRDI QIDQ557795

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

Software engineering; Verification; Assume-guarantee reasoning; Automated theorem proving; Concurrent software; Verification conditions

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Towards Efficient Verification of Systems with Dynamic Process Creation

Uses Software

• SIMPLIFY
• ESC/Java
• Mercator

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