Thread-modular verification for shared-memory programs

DOI10.1007/3-540-45927-8_19MaRDI QIDQ4738361zbMATH OpenFDO

Authors Cormac Flanagan, Stephen N. Freund, Shaz Qadeer

Publication date 11 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2305/23050262.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Modular verification of multithreaded programs
• A modular checker for multithreaded programs
• Thread-modular model checking
• A Basis for Verifying Multi-threaded Programs
• Precise Thread-Modular Verification

Cited in

(20)

• Compositional reasoning for shared-variable concurrent programs
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Rely-guarantee termination and cost analyses of loops with concurrent interleavings
• Parameterized verification of multithreaded software libraries
• Dataflow analysis for datarace-free programs
• Compositionality Entails Sequentializability
• Parameterized Verification of Asynchronous Shared-Memory Systems
• Atomizer: a dynamic atomicity checker for multithreaded programs
• Precise Thread-Modular Verification
• Modular Safety Checking for Fine-Grained Concurrency
• A Basis for Verifying Multi-threaded Programs
• Thread-modular model checking
• A modular checker for multithreaded programs
• Verified Compilation for Shared-Memory C
• A verifying compiler for a multi-threaded object-oriented language
• Modular verification of multithreaded programs
• Fine-grained complexity of safety verification
• Optimistic synchronization-based state-space reduction
• Atomizer: A dynamic atomicity checker for multithreaded programs
• Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning

This page was built for publication: Thread-modular verification for shared-memory programs

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