nuXmv
From MaRDI portal
NuXmv
Cited in
(94)- Linear-time temporal logic with event freezing functions
- Verification of temporal properties of neuronal archetypes modeled as synchronous reactive systems
- A Verified Compositional Algorithm for AI Planning
- Leveraging Horn clause solving for compositional verification of PLC software
- A SAT-based encoding of the one-pass and tree-shaped tableau system for LTL
- Tools and Methods for RTCP-Nets Modeling and Verification
- Evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets
- Aalta
- SMT-based generation of symbolic automata
- SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
- Practical synthesis of reactive systems from LTL specifications via parity games
- IronFleet
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
- Evaluation of cyber security and modelling of risk propagation with Petri nets
- Leviathan
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
- Interpolation and model checking for nonlinear arithmetic
- Sound verification procedures for temporal properties of infinite-state systems
- \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
- Model-based safety assessment of a triple modular generator with xSAP
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- Tightening the contract refinements of a system architecture
- Certifying proofs for SAT-based model checking
- A CTL* Model Checker for Petri Nets
- Sally
- Formal reliability analysis of redundancy architectures
- Infinite-state invariant checking with IC3 and predicate abstraction
- dot
- Optimization modulo the theory of floating-point numbers
- CirCUs
- Rabbit
- BeepBeep
- MARCO
- NuSMV
- ClawZ
- LTSmin
- HRELTL: a temporal logic for hybrid systems
- SPOT
- KRATOS
- SPNP
- FORCE
- MathSAT
- MathSAT5
- BEEM
- LinAIG
- VATA
- TeMP
- TLPVS
- Mcmt
- Rex
- Synthia
- TRP++
- PSync
- PySMT
- HyComp
- SL2SX
- PPlan
- JKind
- Kind 2
- ByMC
- Tip
- Chapar
- Verdi
- CTIGAR
- Symbiotic 2
- SymDIVINE
- Myhill-Nerode
- iSAT
- SAFARI
- AIGER
- ITS-Tools
- Meddly
- lbtt
- Strix
- SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
- What you always wanted to know about model checking of fault-tolerant distributed algorithms
- CompoSAT
- DynAlloy
- Papyrus-RT
- Diagnosability of fair transition systems
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- Owl
- Pardinus: a temporal relational model finder
- Symbolic computation via program transformation
- Btor2Tools
- Satisfiability checking for mission-time \textsf{LTL} (MLTL)
- SAT solver management strategies in IC3: an experimental approach
- Component-wise incremental LTL model checking
- Ivy
- Deadlock in packet switching networks
- The refinement calculus of reactive systems
- Propositional gossip protocols
- OCRA
This page was built for software: nuXmv
