NuSMV: A new symbolic model checker
From MaRDI portal
Publication:1856168
DOI10.1007/s100090050046zbMath1059.68582OpenAlexW2001289891WikidataQ62041431 ScholiaQ62041431MaRDI QIDQ1856168
Fausto Giunchiglia, Alessandro Cimatti, Marco Roveri, Edmund M. Clarke
Publication date: 2000
Published in: International Journal on Software Tools for Technology Transfer. STTT (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s100090050046
Related Items (48)
Automata Theory and Model Checking ⋮ Model Checking of Biological Systems ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ Model checking and strategy synthesis for multi-agent systems for resource allocation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Symbolic synthesis of masking fault-tolerant distributed programs ⋮ Formal verification for event stream processing: model checking of BeepBeep stream processing pipelines ⋮ Verifying a scheduling protocol of safety-critical systems ⋮ On the expressivity and complexity of quantitative branching-time temporal logics ⋮ Agent planning programs ⋮ Symbolic Fault Tree Analysis for Reactive Systems ⋮ MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs ⋮ Unnamed Item ⋮ PuRSUE -- from specification of robotic environments to synthesis of controllers ⋮ The Birth of Model Checking ⋮ Optimal mixed discrete-continuous planning for linear hybrid systems ⋮ An explicit transition system construction approach to LTL satisfiability checking ⋮ An analytic tableau calculus for a temporalised belief logic ⋮ Linear temporal logic symbolic model checking ⋮ Computation Tree Regular Logic for Genetic Regulatory Networks ⋮ Boosting Lazy Abstraction for SystemC with Partial Order Reduction ⋮ Formal semantics and verification of network-based biocomputation circuits ⋮ Incremental methods for checking real-time consistency ⋮ CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks ⋮ Symbolic State-Space Generation of Asynchronous Systems Using Extensible Decision Diagrams ⋮ Test generation from P systems using model checking ⋮ Model-based safety assessment of a triple modular generator with xSAP ⋮ Formal Verification Based on Guided Random Walks ⋮ Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking ⋮ Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking ⋮ From Sequential Extended Regular Expressions to NFA with Symbolic Labels ⋮ FORMAL VERIFICATION OF P SYSTEMS USING SPIN ⋮ A Graph Transformation-Based Approach to Formal Modeling and Verification of Workflows ⋮ Tools and Methods for RTCP-Nets Modeling and Verification ⋮ NuSMV ⋮ Before and after vacuity ⋮ Game-theoretic simulation checking tool ⋮ BDD-based decision procedures for the modal logic K ★ ⋮ Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation ⋮ Unnamed Item ⋮ Verification from Declarative Specifications Using Logic Programming ⋮ Evaluation of cyber security and modelling of risk propagation with Petri nets ⋮ Formal Analysis of Workflows Using UML 2.0 Activities and Graph Transformation Systems ⋮ Interactive verification of architectural design patterns in FACTum ⋮ Semantic consistency checking in building ontology from heterogeneous sources ⋮ Language-Oriented Formal Analysis: a Case Study on Protocols and Distributed Systems ⋮ Translating Java for multiple model checkers: The Bandera back-end
Uses Software
This page was built for publication: NuSMV: A new symbolic model checker
