Model checking with bounded context switching

DOI10.1007/S00165-010-0160-5MaRDI QIDQ539429zbMATH OpenOpenAlexFDO

Authors Gerard J. Holzmann, Mihai Florian

Publication date 30 May 2011

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-010-0160-5

zbMATH Keywords

depth-first searchsoftware verificationpartial order reductionbitstate hashingbounded context-switchinglogic model checking

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

• Tools and Algorithms for the Construction and Analysis of Systems
• On the Complexity of Bounded Context Switching.
• Bounded model checking using satisfiability solving
• scientific article; zbMATH DE number 910719
• Computer Aided Verification

Cites work

• scientific article; zbMATH DE number 1069483 (Why is no real title available?)
• Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
• Space/time trade-offs in hash coding with allowable errors
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(2)

• Explicit-state model checking
• On the Complexity of Bounded Context Switching.

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: Model checking with bounded context switching

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