GSTE is partitioned model checking

DOI10.1007/S10703-007-0036-3MaRDI QIDQ2385196zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• Computer Aided Verification
• Computer Aided Verification
• FM 2005: Formal Methods
• scientific article; zbMATH DE number 1759610
• Partitioned PLTL model-checking for refined transition systems
• Terminal satisfiability in GSTE
• scientific article; zbMATH DE number 898449
• Consistent partial model checking
• A partial approach to model checking
• scientific article; zbMATH DE number 5636822

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1670781 (Why is no real title available?)
• scientific article; zbMATH DE number 1670790 (Why is no real title available?)
• scientific article; zbMATH DE number 1701767 (Why is no real title available?)
• scientific article; zbMATH DE number 1705167 (Why is no real title available?)
• scientific article; zbMATH DE number 177248 (Why is no real title available?)
• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• scientific article; zbMATH DE number 1979544 (Why is no real title available?)
• scientific article; zbMATH DE number 1979546 (Why is no real title available?)
• scientific article; zbMATH DE number 1863179 (Why is no real title available?)
• scientific article; zbMATH DE number 2102706 (Why is no real title available?)
• scientific article; zbMATH DE number 2102710 (Why is no real title available?)
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)
• A scalable parallel algorithm for reachability analysis of very large circuits
• A work-efficient distributed algorithm for reachability analysis.
• An automata-theoretic approach to branching-time model checking
• Computer Aided Verification
• Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
• From pre-historic to post-modern symbolic model checking
• Improved symbolic verification using partitioning techniques
• Model checking of safety properties
• On bounded specifications
• Reasoning about GSTE assertion graphs
• Reasoning about infinite computations
• Symbolic model checking: \(10^{20}\) states and beyond
• ``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking

Cited in

(5)

• Terminal satisfiability in GSTE
• Computer Aided Verification
• Computer Aided Verification
• Symbolic trajectory evaluation
• A transformation-based approach to implication of GSTE assertion graphs

Describes a project that uses

Uses Software

• NuSMV
• SPIN

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

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