GSTE is partitioned model checking

DOI10.1007/S10703-007-0036-3zbMATH Open1129.68044OpenAlexW2166606799MaRDI QIDQ2385196FDOQ2385196

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

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

zbMATH Keywords

Symbolic model checkingGSTEProperty-driven partitioning

Mathematics Subject Classification ID

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

Cites Work

• Symbolic model checking: \(10^{20}\) states and beyond
• Title not available (Why is that?)
• Title not available (Why is that?)
• From pre-historic to post-modern symbolic model checking
• Reasoning about infinite computations
• An automata-theoretic approach to branching-time model checking
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Model checking of safety properties
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computer Aided Verification
• Reasoning about GSTE assertion graphs
• ``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
• On bounded specifications
• Title not available (Why is that?)
• Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
• A scalable parallel algorithm for reachability analysis of very large circuits
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Improved symbolic verification using partitioning techniques
• A work-efficient distributed algorithm for reachability analysis.

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

Uses Software

• SPIN
• NuSMV

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)