Combining symmetry reduction and under-approximation for symbolic model checking

DOI10.1007/S10703-005-2246-XzbMATH Open1085.68086OpenAlexW2040904498MaRDI QIDQ816210FDOQ816210

Authors: Sharon Barner, Orna Grumberg 

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

Recommendations

• scientific article; zbMATH DE number 1903347
• scientific article; zbMATH DE number 1487862
• scientific article; zbMATH DE number 1796126
• scientific article; zbMATH DE number 2087620
• Efficient symmetry reduction and the use of state symmetries for symbolic model checking

zbMATH Keywords

symmetry reductionsymbolic model checkinghintsunder-approximation

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (5)

• Employing symmetry reductions in model checking
• Context-aware counter abstraction
• Correct Hardware Design and Verification Methods
• Efficient approximate verification of B and Z models via symmetry markers
• Title not available (Why is that?)

Uses Software

• CESAR

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

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