GSTE is partitioned model checking

DOI10.1007/s10703-007-0036-3zbMath1129.68044OpenAlexW2166606799MaRDI QIDQ2385196

Moshe Y. Vardi, Stefano Tonetta, Roberto Sebastiani, Eli Singerman

Publication date: 11 October 2007

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

Full work available at URL: https://doi.org/10.1007/s10703-007-0036-3

zbMATH Keywords

Symbolic model checkingGSTEProperty-driven partitioning

Mathematics Subject Classification ID

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

Related Items (1)

Symbolic Trajectory Evaluation

Uses Software

• SPIN
• NuSMV

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Symbolic model checking: \(10^{20}\) states and beyond
• Reasoning about infinite computations
• A scalable parallel algorithm for reachability analysis of very large circuits
• From pre-historic to post-modern symbolic model checking
• On Bounded Specifications
• Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata
• Computer Aided Verification
• An automata-theoretic approach to branching-time model checking
• Correct Hardware Design and Verification Methods
• Correct Hardware Design and Verification Methods
• Correct Hardware Design and Verification Methods
• Computer Aided Verification
• Model checking of safety properties

This page was built for publication: GSTE is partitioned model checking