Ensuring completeness of symbolic verification methods for infinite-state systems

DOI10.1016/S0304-3975(00)00105-5zbMath0973.68146MaRDI QIDQ5941104

Bengt Jonsson, Parosh Aziz Abdulla

Publication date: 20 August 2001

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00105-5

zbMATH Keywords

model checking; infinite-state systems; reachability analysis; symbolic verification

Mathematics Subject Classification ID

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

Related Items

Unnamed Item, Well-structured transition systems everywhere!, Linearizing well quasi-orders and bounding the length of bad sequences, A note on well quasi-orderings for powersets, Well (and Better) Quasi-Ordered Transition Systems

Uses Software

• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Undecidable verification problems for programs with unreliable channels
• Decidability of a temporal logic problem for Petri nets
• Combining partial-order reductions with on-the-fly model-checking.
• Reduction and covering of infinite reachability trees
• Local model checking for infinite state spaces
• Deciding bisimulation equivalences for a class of non-finite-state programs
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Verifying programs with unreliable channels
• Graph-Based Algorithms for Boolean Function Manipulation
• Distributed cooperation with action systems
• A really temporal logic
• Reasoning about systems with many processes
• Deciding properties of integral relational automata
• Hybrid automata with finite bisimulations
• Ordering by Divisibility in Abstract Algebras
• Symbolic model checking with rich assertional languages
• Decidability of bisimulation equivalence for normed pushdown processes