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
• Proving stabilization of biological systems
• 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
• A logical framework for systems biology
• Fairness modulo theory: a new approach to LTL software model checking
• Model checking approach to automated planning
• Verification and enforcement of access control policies
• Automated formal analysis and verification: an overview
• A new rule for LTL tableaux
• 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
• Formal verification of timed synchronous dataflow graphs using Lustre
• A bounded model checker for three-valued abstractions of concurrent software systems
• 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
• Computation tree logic and NuSMV model checker
• From Philosophical to Industrial Logics
• Title not available (Why is that?)
• Integrating topological proofs with model checking to instrument iterative design
• 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
• Kernel P systems modelling, testing and verification -- sorting case study
• Title not available (Why is that?)
• Symbolic Model Checking of Logics with Actions
• A formalisation of violation, error recovery, and enforcement in the bit transmission problem
• Timed hyperproperties
• SMT-based scenario verification for hybrid systems
• Automata theory and model checking
• Title not available (Why is that?)
• Not all bugs are created equal, but robust reachability can tell the difference
• Model checking \(\omega \)-regular properties with decoupled search
• On regular temporal logics with past
• Representing and Reasoning about Temporal Granularities
• CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks
• Model Checking on Trees with Path Equivalences
• Formal dependability modeling and analysis: a survey
• A Multi-Core Solver for Parity Games
• Action language verifier: An infinite-state model checker for reactive software specifications
• Conformant planning via symbolic model checking and heuristic search
• Incremental learning-based testing for reactive systems
• Verifying data refinements using a model checker
• Applying model-checking to solve queries on semistructured data
• Representing and reasoning with qualitative preferences for compositional systems
• BDD-based symbolic model checking
• The formal-CAFE methodology and model checking patterns in the specification of e-commerce systems
• A New Approach to Bounded Model Checking for Branching Time Logics
• Title not available (Why is that?)
• Temporal property verification as a program analysis task
• On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
• Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition
• Application of Wu's method to symbolic model checking
• Early verification and validation of mission critical systems
• From NuSMV to SPIN: Experiences with model checking flight guidance systems
• MAVEN: Modular aspect verification and interference analysis
• Theorem proving for pointwise metric temporal logic over the naturals via translations
• Using Bounded Model Checking to Verify Consensus Algorithms
• Program repair without regret
• Diagnosability of fair transition systems
• MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs
• Deciding Bit-Vector Formulas with mcSAT
• Testing Distributed Systems Through Symbolic Model Checking
• HRELTL: a temporal logic for hybrid systems
• Agent planning programs
• An executable specification of a formal argumentation protocol
• Formal verification technique for grid service chain model and its application

This page was built for software: NuSMV