Verification of asynchronous programs with nested locks

DOI10.4230/LIPICS.FSTTCS.2017.11MaRDI QIDQ5136300zbMATH OpenOpenAlexFDO

Authors Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan, Prakash Saivasan

Publication date 25 November 2020

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2018/8410/pdf/LIPIcs-FSTTCS-2017-11.pdf/

zbMATH Keywords

reachability problemasynchronous programsnested locks

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• General decidability results for asynchronous shared-memory programs: higher-order and beyond
• scientific article; zbMATH DE number 7682282
• Reachability under contextual locking
• Reachability under contextual locking
• Dealing with Priorities and Locks for Concurrent Programs

Cites work

• Analyzing Asynchronous Programs with Preemption
• Analyzing Real-Time Event-Driven Programs
• CONCUR 2005 – Concurrency Theory
• Computer Aided Verification
• Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors
• Context-bounded analysis for concurrent programs with dynamic creation of threads
• Delay-bounded scheduling
• Interprocedural analysis of asynchronous programs
• Join-Lock-Sensitive Forward Reachability Analysis for Concurrent Programs with Dynamic Process Creation
• Model Checking Multithreaded Programs with Asynchronous Atomic Methods
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(9)

• Compositional Bitvector Analysis for Concurrent Programs with Nested Locks
• scientific article; zbMATH DE number 7561313 (Why is no real title available?)
• General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
• Reachability under contextual locking
• Deciding branching time properties for asynchronous programs
• Model Checking Multithreaded Programs with Asynchronous Atomic Methods
• Analyzing Asynchronous Programs with Preemption
• Nested, but separate: isolating unrelated critical sections in real-time nested locking
• Verifying liveness for asynchronous programs

Describes a project that uses

Uses Software

• Program-Conflict-Analysis

This page was built for publication: Verification of asynchronous programs with nested locks

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