Concurrent software verification with states, events, and deadlocks
DOI10.1007/S00165-005-0071-ZzbMATH Open1103.68609OpenAlexW2159031014MaRDI QIDQ2432214FDOQ2432214
Authors: Natasha Sharygina, Nishant Sinha, Sagar Chaki, Edmund Clarke, Joël Ouaknine 
Publication date: 25 October 2006
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-005-0071-z
Recommendations
model checkingtemporal logiccompositional reasoningdeadlockconcurrent softwarecounterexample-guided abstraction refinementstates and events
Cited In (14)
- Simulation for lattice-valued doubly labeled transition systems
- Partial Order Reduction for State/Event LTL
- State/Event Software Verification for Branching-Time Specifications
- A formal model for service-oriented interactions
- Partial order reduction for state/event LTL with application to component-interaction automata
- SAT-solving in CSP trace refinement
- A rewriting-based model checker for the linear temporal logic of rewriting
- Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving
- Tighter reachability criteria for deadlock-freedom analysis
- Using heuristic search for finding deadlocks in concurrent systems
- Local Nontermination Detection for Parallel C++ Programs
- Verification, Model Checking, and Abstract Interpretation
- Automated compositional abstraction refinement for concurrent C programs: a two-level approach
- Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
Uses Software
This page was built for publication: Concurrent software verification with states, events, and deadlocks
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2432214)
