2-valued and 3-valued abstraction-refinement in model checking

DOI10.3233/978-1-60750-100-8-105MaRDI QIDQ3060979zbMATH OpenFDO

Authors Orna Grumberg

Publication date 13 December 2010

Full work available at URL https://doi.org/10.3233/978-1-60750-100-8-105

zbMATH Keywords

3-valued abstractionCEGARcompositional model checkingmodel checkingrefinementTVAR

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• The abstraction-refinement framework in model checking
• 3-valued abstraction: More precision at less cost
• Parameterisation of three-valued abstractions
• scientific article; zbMATH DE number 1953032
• A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.

Cited in

(13)

• Parameterisation of three-valued abstractions
• Bonsai: cutting models down to size
• Compositional Verification and 3-Valued Abstractions Join Forces
• Property Driven Three-Valued Model Checking on Hybrid Automata
• A framework for compositional verification of multi-valued systems via abstraction-refinement
• Don't know for multi-valued systems
• scientific article; zbMATH DE number 1953032 (Why is no real title available?)
• A game-based framework for CTL counterexamples and 3-valued abstraction-refinement
• Tools and Algorithms for the Construction and Analysis of Systems
• The abstraction-refinement framework in model checking
• A game-based framework for CTL counterexamples and 3-valued abstraction-refinement.
• Spotlight abstraction in model checking real-time task schedulability
• 3-valued abstraction: More precision at less cost

Describes a project that uses

Uses Software

• Chaff
• BerkMin

This page was built for publication: 2-valued and 3-valued abstraction-refinement in model checking

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