Model Checking Multithreaded Programs with Asynchronous Atomic Methods

DOI10.1007/11817963_29MaRDI QIDQ5756745zbMATH OpenOpenAlexFDO

Authors Koushik Sen, Mahesh Viswanathan

Publication date 5 September 2007

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11817963_29

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 1982207
• Verification of asynchronous programs with nested locks
• Model checking concurrent programs
• scientific article; zbMATH DE number 1670562

Cited in

(17)

• scientific article; zbMATH DE number 7561313 (Why is no real title available?)
• General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
• On the Reachability Analysis of Acyclic Networks of Pushdown Systems
• Realizability of Concurrent Recursive Programs
• On functions weakly computable by pushdown Petri nets and related systems
• Deciding branching time properties for asynchronous programs
• Verification of asynchronous programs with nested locks
• General decidability results for asynchronous shared-memory programs: higher-order and beyond
• Analyzing Real-Time Event-Driven Programs
• Multiparty half-duplex systems and synchronous communications
• Budget-bounded model-checking pushdown systems
• Some complexity results for stateful network verification
• Context-Bounded Analysis of Concurrent Queue Systems
• Towards generalised half-duplex systems
• Data flow analysis of asynchronous systems using infinite abstract domains
• Analyzing pushdown systems with stack manipulation
• Reasoning about threads with bounded lock chains

Describes a project that uses

Uses Software

• SLAM

This page was built for publication: Model Checking Multithreaded Programs with Asynchronous Atomic Methods

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