Concurrent software verification with states, events, and deadlocks

DOI10.1007/S00165-005-0071-ZMaRDI QIDQ2432214zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

model checkingtemporal logiccompositional reasoningdeadlockconcurrent softwarecounterexample-guided abstraction refinementstates and events

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Integrated Formal Methods
• Automated compositional abstraction refinement for concurrent C programs: a two-level approach
• Efficient verification of sequential and concurrent C programs
• scientific article; zbMATH DE number 1670562
• Symbolic Counter Abstraction for Concurrent Software

Cited in

(14)

• Simulation for lattice-valued doubly labeled transition systems
• Partial Order Reduction for State/Event LTL
• A formal model for service-oriented interactions
• State/Event Software Verification for Branching-Time Specifications
• 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

Describes a project that uses

Uses Software

• MAGIC
• Bandera
• Zing

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)