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
• What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
• Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets
• Propositional gossip protocols
• Symbolic computation via program transformation
• Evaluation of cyber security and modelling of risk propagation with Petri nets
• A CTL* Model Checker for Petri Nets
• A Verified Compositional Algorithm for AI Planning
• Title not available (Why is that?)
• 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
• Diagnosability of fair transition systems
• HRELTL: a temporal logic for hybrid systems
• Tools and Methods for RTCP-Nets Modeling and Verification
• Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
• 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
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Verification of Temporal Properties of Neuronal Archetypes Modeled as Synchronous Reactive Systems
• Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
• 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