Model Checking Concurrent Programs
From MaRDI portal
Publication:3176376
DOI10.1007/978-3-319-10575-8_18zbMath1392.68251OpenAlexW2806836266MaRDI QIDQ3176376
Tayssir Touili, Vineet Kahlon, Aarti Gupta, Shaz Qadeer
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_18
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Symbolic predictive analysis for concurrent programs
- Fences in weak memory models
- Local proofs for global safety properties
- Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
- Verifying parallel programs with dynamic communication structures
- Bounded Phase Analysis of Message-Passing Programs
- A generic approach to the static analysis of concurrent programs with procedures
- Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs
- Reasoning about Threads with Bounded Lock Chains
- On the analysis of interacting pushdown systems
- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
- Effective Program Verification for Relaxed Memory Models
- On the Reachability Analysis of Acyclic Networks of Pushdown Systems
- Trace-Based Symbolic Analysis for Atomicity Violations
- Forward Analysis of Depth-Bounded Processes
- Meta-analysis for Atomicity Violations under Nested Locking
- Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
- Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints
- Verifying Parallel Programs with Dynamic Communication Structures
- Time, clocks, and the ordering of events in a distributed system
- Compositional Bitvector Analysis for Concurrent Programs with Nested Locks
- A calculus of atomic actions
- Dynamic partial-order reduction for model checking software
- CONCUR 2004 - Concurrency Theory
- Compositional Shape Analysis by Means of Bi-Abduction
- Predicate abstraction and refinement for verifying multi-threaded programs
- On interference abstractions
- Parametric and Sliced Causality
- Peephole Partial Order Reduction
- A Generic Approach to the Static Analysis of Concurrent Programs with Procedures
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Reachability under Contextual Locking
- Reachability under Contextual Locking
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Reachability analysis of pushdown automata: Application to model-checking
