nuXmv

swMATH18526MaRDI QIDQ30365FDOQ30365

Author name not available (Why is that?)

Cited In (38)

• Higher-order quantifier elimination, counter simulations and fault-tolerant systems
• Pardinus: a temporal relational model finder
• Satisfiability checking for mission-time \textsf{LTL} (MLTL)
• Practical synthesis of reactive systems from LTL specifications via parity games
• Interpolation and model checking for nonlinear arithmetic
• Sound verification procedures for temporal properties of infinite-state systems
• The refinement calculus of reactive systems
• Propositional gossip protocols
• Symbolic computation via program transformation
• Verification of temporal properties of neuronal archetypes modeled as synchronous reactive systems
• Evaluation of cyber security and modelling of risk propagation with Petri nets
• A CTL* Model Checker for Petri Nets
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• A Verified Compositional Algorithm for AI Planning
• Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
• Certifying proofs for SAT-based model checking
• Model-based safety assessment of a triple modular generator with xSAP
• Optimization modulo the theory of floating-point numbers
• Deadlock in packet switching networks
• Tightening the contract refinements of a system architecture
• Evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets
• Diagnosability of fair transition systems
• HRELTL: a temporal logic for hybrid systems
• Tools and Methods for RTCP-Nets Modeling and Verification
• Linear-time temporal logic with event freezing functions
• Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
• 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
• SMT-based generation of symbolic automata
• SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
• Infinite-state invariant checking with IC3 and predicate abstraction
• What you always wanted to know about model checking of fault-tolerant distributed algorithms
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Component-wise incremental LTL model checking
• SAT-based explicit \(\mathsf{LTL}_f\) satisfiability checking
• Formal reliability analysis of redundancy architectures
• SAT-based explicit LTL reasoning and its application to satisfiability checking
• SAT solver management strategies in IC3: an experimental approach

This page was built for software: nuXmv