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

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