The following pages link to NuSMV (Q16316):
Displaying 50 items.
- Before and after vacuity (Q1028732) (← links)
- An executable specification of a formal argumentation protocol (Q1028953) (← links)
- A rigorous methodology for specification and verification of business processes (Q1037243) (← links)
- On the expressivity and complexity of quantitative branching-time temporal logics (Q1401306) (← links)
- Verifying the IEEE 1394 fireWire tree identify protocol with SMV (Q1402475) (← links)
- A compiler for MSVL and its applications (Q1630985) (← links)
- Falsification of combined invariance and reachability specifications in hybrid control systems (Q1693831) (← links)
- Fairness modulo theory: a new approach to LTL software model checking (Q1702910) (← links)
- From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories (Q1704601) (← links)
- An explicit transition system construction approach to LTL satisfiability checking (Q1707341) (← links)
- A first-order coalition logic for BDI-agents (Q1712430) (← links)
- Applying model-checking to solve queries on semistructured data (Q1749228) (← links)
- A bounded model checker for three-valued abstractions of concurrent software systems (Q1784791) (← links)
- Modeling and querying biomolecular interaction networks (Q1884862) (← links)
- Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice (Q1884863) (← links)
- Symbolic synthesis of masking fault-tolerant distributed programs (Q1938357) (← links)
- Formal analysis of piecewise affine systems through formula-guided refinement (Q1939637) (← links)
- Formal verification based on Boolean expression diagrams (Q1954165) (← links)
- Spiking neural P systems: matrix representation and formal verification (Q1983014) (← links)
- Search-based testing in membrane computing (Q1983028) (← links)
- Model-based safety assessment of a triple modular generator with xSAP (Q2026377) (← links)
- Formal verification of timed synchronous dataflow graphs using lustre (Q2043814) (← links)
- TOrPEDO : witnessing model correctness with topological proofs (Q2065548) (← links)
- Diagnosability verification using LTL model checking (Q2081084) (← links)
- Pardinus: a temporal relational model finder (Q2102939) (← links)
- What is a cell cycle checkpoint? The \texttt{TotemBioNet} answer (Q2110690) (← links)
- Automatic synthesis of transiently correct network updates via Petri games (Q2117163) (← links)
- The ASMETA approach to safety assurance of software systems (Q2117597) (← links)
- Greening R. Thomas' framework with environment variables: a divide and conquer approach (Q2142101) (← links)
- Aeon 2021: bifurcation decision trees in Boolean networks (Q2142120) (← links)
- Social bot detection as a temporal logic model checking problem (Q2148829) (← links)
- Diagnosability of fair transition systems (Q2152493) (← links)
- Formal model of the interplay between TGF-\(\beta 1\) and MMP-9 and their dynamics in hepatocellular carcinoma (Q2160695) (← links)
- Collaborative models for autonomous systems controller synthesis (Q2198131) (← links)
- PuRSUE -- from specification of robotic environments to synthesis of controllers (Q2198133) (← links)
- Theorem proving for pointwise metric temporal logic over the naturals via translations (Q2228435) (← links)
- Toward model selection by formal methods (Q2229136) (← links)
- Strategies, model checking and branching-time properties in Maude (Q2239275) (← links)
- Verification and enforcement of access control policies (Q2248087) (← links)
- Model checking approach to automated planning (Q2248102) (← links)
- On the order of test goals in specification-based testing (Q2270689) (← links)
- Bio-PEPA: A framework for the modelling and analysis of biological systems (Q2271444) (← links)
- Translating Xd-C programs to MSVL programs (Q2290648) (← links)
- Performance heuristics for GR(1) synthesis and related algorithms (Q2303873) (← links)
- Parameterized synthesis of self-stabilizing protocols in symmetric networks (Q2303887) (← links)
- Evaluation of cyber security and modelling of risk propagation with Petri nets (Q2333477) (← links)
- SAT-based explicit LTL reasoning and its application to satisfiability checking (Q2335900) (← links)
- A verification-driven framework for iterative design of controllers (Q2335947) (← links)
- Interactive verification of architectural design patterns in FACTum (Q2335950) (← links)
- Semantic consistency checking in building ontology from heterogeneous sources (Q2336201) (← links)
