scientific article; zbMATH DE number 2102712

zbMath1046.68583MaRDI QIDQ4818796

Patrice Godefroid, Glenn Bruns

Publication date: 24 September 2004

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (38)

Integrating Topological Proofs with Model Checking to Instrument Iterative Design ⋮ An abstraction-refinement methodology for reasoning about network games ⋮ Abstraction and Abstraction Refinement ⋮ The Complexity of Linear-Time Temporal Logic Model Repair ⋮ Bonsai: Cutting Models Down to Size ⋮ When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus ⋮ An abstract interpretation toolkit for \(\mu\)CRL ⋮ Inherent Vacuity in Lattice Automata ⋮ On the consistency, expressiveness, and precision of partial modeling formalisms ⋮ Be lazy and don't care: faster CTL model checking for recursive state machines ⋮ Unnamed Item ⋮ Information Exchange Between Over- and Underapproximating Software Analyses ⋮ Compositional Specification in Rewriting Logic ⋮ Multi-valued model checking games ⋮ Latticed Simulation Relations and Games ⋮ Computation tree logic model checking based on multi-valued possibility measures ⋮ Model Checking Recursive Programs with Exact Predicate Abstraction ⋮ On model checking multiple hybrid views ⋮ 3-valued abstraction: More precision at less cost ⋮ Unnamed Item ⋮ Model-Checking View-Based Partial Specifications ⋮ Unnamed Item ⋮ Static analysis of topology-dependent broadcast networks ⋮ Compositional verification and 3-valued abstractions join forces ⋮ A local approach for temporal model checking of Java bytecode ⋮ Multi-robot LTL planning under uncertainty ⋮ Model checking of linear-time properties in multi-valued systems ⋮ Lattice Automata ⋮ Approximate verification of strategic abilities under imperfect information ⋮ Minimizing Deterministic Lattice Automata ⋮ On the Complexity of Semantic Self-minimization ⋮ Logical vs. behavioural specifications ⋮ TOrPEDO : witnessing model correctness with topological proofs ⋮ Don’t Know for Multi-valued Systems ⋮ Bounded Model Checking for Partial Kripke Structures ⋮ A verification-driven framework for iterative design of controllers ⋮ On finite-state approximants for probabilistic computation tree logic ⋮ A framework for compositional verification of multi-valued systems via abstraction-refinement

This page was built for publication: