scientific article; zbMATH DE number 177237

MaRDI QIDQ4037087zbMATH OpenFDO

Authors Antti Valmari

Publication date 18 May 1993

zbMATH Keywords

automatic verification of concurrent systemslinear time temporal logic specificationsreduced state space

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 177511
• scientific article; zbMATH DE number 1059329
• A stubborn attack on state explosion
• Publication:4507831
• On Stubborn Sets in the Verification of Linear Time Temporal Properties

Cited in

(26)

• Verification of distributed programs using representative interleaving sequences
• A technique of state space search based on unfolding
• Using integer programming to verify general safety and liveness properties
• Compositional verification of asynchronous concurrent systems using CADP
• Exploiting interleaving semantics in symbolic state-space generation
• Modular synthesis of timed circuits using partial orders on LPNs
• Stubborn sets for simple linear time properties
• scientific article; zbMATH DE number 1799526 (Why is no real title available?)
• States that are far from being stabilizer states
• The Birth of Model Checking
• scientific article; zbMATH DE number 177511 (Why is no real title available?)
• scientific article; zbMATH DE number 1059329 (Why is no real title available?)
• scientific article; zbMATH DE number 1515298 (Why is no real title available?)
• scientific article; zbMATH DE number 744059 (Why is no real title available?)
• Model-checking for real-time systems
• Formal relationships between geometrical and classical models for concurrency
• Covering steps graphs of time Petri nets
• scientific article; zbMATH DE number 967392 (Why is no real title available?)
• Comparing transition systems with independence and asynchronous transition systems
• On Stubborn Sets in the Verification of Linear Time Temporal Properties
• Integer programming in the analysis of concurrent systems
• Bounded-memory algorithms for verification on-the-fly
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• A stubborn attack on state explosion
• Specification and automatic verification of self-timed queues
• Combining partial-order reductions with on-the-fly model-checking.

This page was built for publication:

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