NuSMV

swMATH4131MaRDI QIDQ16316FDOQ16316

Author name not available (Why is that?)

Described by source

• NuSMV: A new symbolic model checker

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

• Spiking neural P systems: matrix representation and formal verification
• Search-based testing in membrane computing
• Pardinus: a temporal relational model finder
• Performance heuristics for GR(1) synthesis and related algorithms
• Finding State Solutions to Temporal Logic Queries
• Towards light-weight probabilistic model checking
• Kernel P systems: from modelling to verification and testing
• Title not available (Why is that?)
• Automatic synthesis of transiently correct network updates via Petri games
• The ASMETA approach to safety assurance of software systems
• An explicit transition system construction approach to LTL satisfiability checking
• Toward model selection by formal methods
• Interactive verification of architectural design patterns in FACTum
• Evaluation of cyber security and modelling of risk propagation with Petri nets
• Test generation from P systems using model checking
• Kernel P Systems Modelling, Testing and Verification - Sorting Case Study
• Fairness modulo theory: a new approach to LTL software model checking
• Title not available (Why is that?)
• Integrating Topological Proofs with Model Checking to Instrument Iterative Design
• Proving Stabilization of Biological Systems
• Model checking approach to automated planning
• Verification and enforcement of access control policies
• Automated formal analysis and verification: an overview
• Formal verification based on Boolean expression diagrams
• Aeon 2021: bifurcation decision trees in Boolean networks
• Greening R. Thomas' framework with environment variables: a divide and conquer approach
• Model-based safety assessment of a triple modular generator with xSAP
• Verification, Model Checking, and Abstract Interpretation
• Strategies, model checking and branching-time properties in Maude
• A Cookbook for Temporal Conceptual Data Modelling with Description Logics
• Social bot detection as a temporal logic model checking problem
• Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints
• A bounded model checker for three-valued abstractions of concurrent software systems
• Formal verification of timed synchronous dataflow graphs using lustre
• Formal model of the interplay between TGF-\(\beta 1\) and MMP-9 and their dynamics in hepatocellular carcinoma
• Analysis of UML Activities Using Dynamic Meta Modeling
• A rigorous methodology for specification and verification of business processes
• From Philosophical to Industrial Logics
• Title not available (Why is that?)
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• A verification-driven framework for iterative design of controllers
• Falsification of combined invariance and reachability specifications in hybrid control systems
• Title not available (Why is that?)
• What is a cell cycle checkpoint? The \texttt{TotemBioNet} answer
• Diagnosability verification using LTL model checking
• CTL Model-Checking with Graded Quantifiers
• From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
• A resolution calculus for the branching-time temporal logic CTL
• Collaborative models for autonomous systems controller synthesis
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• Title not available (Why is that?)
• Verification of SpecC using predicate abstraction
• TOrPEDO : witnessing model correctness with topological proofs
• A first-order coalition logic for BDI-agents
• Multi-Valued Reasoning about Reactive Systems
• A Logical Framework for Systems Biology
• Title not available (Why is that?)
• Title not available (Why is that?)
• Symbolic Model Checking of Logics with Actions
• Bio-PEPA: A framework for the modelling and analysis of biological systems
• Model Checking Contracts – A Case Study
• Verification: Theory and Practice
• 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
• Translating Xd-C programs to MSVL programs
• The Birth of Model Checking
• NuMDG: a new tool for multiway decision graphs construction
• 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
• Symbolic Model Checking for Temporal-Epistemic Logic
• 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
• Computer Aided Verification
• Model Checking of Biological Systems
• Bounded LTL model checking with stable models
• 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
• Symbolic Fault Tree Analysis for Reactive Systems
• 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
• Modeling and Analysis of Gene Regulatory Networks
• Experimental Evaluation of Classical Automata Constructions
• Title not available (Why is that?)
• Data structures for symbolic multi-valued model-checking
• SAT-solving in CSP trace refinement
• A decidability result for the model checking of infinite-state systems
• Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking
• Recasting Constraint Automata into Büchi Automata

This page was built for software: NuSMV