Combining symmetry reduction and under-approximation for symbolic model checking

DOI10.1007/s10703-005-2246-xzbMath1085.68086OpenAlexW2040904498MaRDI QIDQ816210

Orna Grumberg, Sharon Barner

Publication date: 20 February 2006

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-005-2246-x

zbMATH Keywords

symbolic model checkingsymmetry reductionhintsunder-approximation

Mathematics Subject Classification ID

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

Related Items (2)

Context-aware counter abstraction ⋮ Efficient approximate verification of B and Z models via symmetry markers

Uses Software

• CESAR

Cites Work

• Characterizing finite Kripke structures in propositional temporal logic
• Symbolic model checking: \(10^{20}\) states and beyond
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• “Sometimes” and “not never” revisited
• Verifying temporal properties without temporal logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Combining symmetry reduction and under-approximation for symbolic model checking