NuSMV

swMATH4131MaRDI QIDQ16316FDOQ16316

Author name not available (Why is that?)

Official website: http://nusmv.fbk.eu/

Described by source

• NuSMV: A new symbolic model checker

Cited In (only showing first 100 items - show all)

• Symbolic synthesis of masking fault-tolerant distributed programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• \texttt{VeriSIMPL 2}: an open-source software for the verification of max-plus-linear systems
• Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
• Extracting unsatisfiable cores for LTL via temporal resolution
• The Birth of Model Checking
• Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice
• Linear Encodings of Bounded LTL Model Checking
• PuRSUE -- from specification of robotic environments to synthesis of controllers
• Interrupt timed automata: verification and expressiveness
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Title not available (Why is that?)
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints
• Verification from Declarative Specifications Using Logic Programming
• Strong planning under partial observability
• Analysing sanity of requirements for avionics systems
• Verification of \(\mathrm{EB}^3\) specifications using CADP
• Bounded situation calculus action theories
• Automatic symbolic compositional verification by learning assumptions
• Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
• Bounded Model Checking for Weak Alternating Büchi Automata
• Experimental Evaluation of Classical Automata Constructions
• Data structures for symbolic multi-valued model-checking
• R. Thomas' modeling of biological regulatory networks: Introduction of singular states in the qualitative dynamics
• SAT-solving in CSP trace refinement
• Weak, strong, and strong cyclic planning via symbolic model checking
• Computer Aided Verification
• Counterexamples revisited: principles, algorithms, applications
• Automated Technology for Verification and Analysis
• Title not available (Why is that?)
• Formal analysis of piecewise affine systems through formula-guided refinement
• Before and after vacuity
• Modelling timed reactive systems from natural-language requirements
• Model checking of biological systems
• Modeling and querying biomolecular interaction networks
• Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams
• Verifying the IEEE 1394 fireWire tree identify protocol with SMV
• Symbolic CTL model checking of asynchronous systems using constrained saturation
• Acacia+
• CITP
• CTL-RP
• MinGW
• P-Lingua
• BINSEC/SE
• CAESAR
• PyCUDD
• VCS
• Dynamic Architectures
• FACTum
• Lorel
• C2M
• MSVL
• ASSA-PBN
• CuSNP
• Jass
• PQL
• UMC4M
• JBotSim
• AdamMC
• zUpdate
• Tools and Algorithms for the Construction and Analysis of Systems
• Specifying norm-governed computational societies
• PTrie
• GNA
• Architectural_Design_Patterns
• CompoSAT
• ASMETA
• PuRSUE
• DynAlloy
• FaSTrack
• EPFL
• Papyrus-RT
• VIS
• Time-budgeting: a component based development methodology for real-time embedded systems
• Proof-based verification approaches for dynamic properties: application to the information system domain
• On the verification of very expressive temporal properties of non-terminating Golog programs
• Theory and Applications of Satisfiability Testing
• Verification of Boolean programs with unbounded thread creation
• Title not available (Why is that?)
• Modeling and analysis of gene regulatory networks
• Deductive verification of simple foraging robotic behaviours
• Compressing BMC encodings with QBF
• Verification, Model Checking, and Abstract Interpretation
• Computation Tree Regular Logic for Genetic Regulatory Networks
• An overview of the mCRL2 toolset and its recent advances
• Title not available (Why is that?)
• A compiler for MSVL and its applications
• On the expressivity and complexity of quantitative branching-time temporal logics
• VCS: a verifier for component-based systems
• Translating Xd-C programs to MSVL programs
• NuMDG: a new tool for multiway decision graphs construction
• SPOT
• Alcoa
• DESUMA
• GIDDES
• MCK
• CBMC
• BEEM

This page was built for software: NuSMV