Model checking concurrent programs

DOI10.1007/978-3-319-10575-8_18MaRDI QIDQ3176376zbMATH OpenOpenAlexFDO

Authors Aarti Gupta, Vineet Kahlon, Tayssir Touili, 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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model checking of concurrent algorithms: from Java to C
• CONCUR 2004 - Concurrency Theory
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 2080197 (Why is no real title available?)
• scientific article; zbMATH DE number 1796143 (Why is no real title available?)
• scientific article; zbMATH DE number 2090847 (Why is no real title available?)
• A Generic Approach to the Static Analysis of Concurrent Programs with Procedures
• A calculus of atomic actions
• A generic approach to the static analysis of concurrent programs with procedures
• Bounded phase analysis of message-passing programs
• CONCUR 2004 - Concurrency Theory
• Compositional Bitvector Analysis for Concurrent Programs with Nested Locks
• Compositional shape analysis by means of bi-abduction
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Dynamic partial-order reduction for model checking software
• Effective Program Verification for Relaxed Memory Models
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Fences in weak memory models
• Forward analysis of depth-bounded processes
• Local proofs for global safety properties
• Meta-analysis for Atomicity Violations under Nested Locking
• Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
• On interference abstractions
• On the Reachability Analysis of Acyclic Networks of Pushdown Systems
• On the analysis of interacting pushdown systems
• Parametric and Sliced Causality
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Peephole Partial Order Reduction
• Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints
• Predicate abstraction and refinement for verifying multi-threaded programs
• Reachability analysis of pushdown automata: Application to model-checking
• Reachability under contextual locking
• Reachability under contextual locking
• Reasoning about threads with bounded lock chains
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• Static analysis of run-time errors in embedded critical parallel C programs
• Symbolic predictive analysis for concurrent programs
• Thread-modular abstraction refinement.
• Time, clocks, and the ordering of events in a distributed system
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Trace-based symbolic analysis for atomicity violations
• Verifying Parallel Programs with Dynamic Communication Structures
• Verifying parallel programs with dynamic communication structures

Cited in

(20)

• Temporal Logic for Programmable Logic Controllers
• Modular verification of concurrent programs via sequential model checking
• Underspecified harnesses and interleaved bugs
• Cloud-based verification of concurrent software
• Local Proofs for Linear-Time Properties of Concurrent Programs
• scientific article; zbMATH DE number 1670562 (Why is no real title available?)
• Model checking concurrency and causality
• CONCUR 2004 - Concurrency Theory
• SAT-Based Model Checking
• Model Checking Multithreaded Programs with Asynchronous Atomic Methods
• A formal semantics for debugging synchronous message passing-based concurrent programs
• Model checking concurrent programs with nondeterminism and randomization
• Parallel assertions for architectures with weak memory models
• Reasoning about threads with bounded lock chains
• Modeling and verifying multi-core programs
• scientific article; zbMATH DE number 967185 (Why is no real title available?)
• Modelling concurrency with comtraces and generalized comtraces
• Model checking of concurrent software systems via heuristic-guided SAT solving
• Model checking of concurrent algorithms: from Java to C
• Computer Aided Verification

Describes a project that uses

Uses Software

• MAGIC
• Checkfence
• ISP
• veriSoft

This page was built for publication: Model checking concurrent programs

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