swMATH4131MaRDI QIDQ16316FDOQ16316
Author name not available (Why is that?)
Official website: http://nusmv.fbk.eu/
Cited In (only showing first 100 items - show all)
- Symbolic synthesis of masking fault-tolerant distributed programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- \texttt{VeriSIMPL 2}: an open-source software for the verification of max-plus-linear systems
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
- Extracting unsatisfiable cores for LTL via temporal resolution
- The Birth of Model Checking
- Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice
- Linear Encodings of Bounded LTL Model Checking
- PuRSUE -- from specification of robotic environments to synthesis of controllers
- Interrupt timed automata: verification and expressiveness
- Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
- Title not available (Why is that?)
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints
- Verification from Declarative Specifications Using Logic Programming
- Strong planning under partial observability
- Analysing sanity of requirements for avionics systems
- Verification of \(\mathrm{EB}^3\) specifications using CADP
- Bounded situation calculus action theories
- Automatic symbolic compositional verification by learning assumptions
- Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
- Bounded Model Checking for Weak Alternating Büchi Automata
- Experimental Evaluation of Classical Automata Constructions
- Data structures for symbolic multi-valued model-checking
- R. Thomas' modeling of biological regulatory networks: Introduction of singular states in the qualitative dynamics
- SAT-solving in CSP trace refinement
- Weak, strong, and strong cyclic planning via symbolic model checking
- Computer Aided Verification
- Counterexamples revisited: principles, algorithms, applications
- Automated Technology for Verification and Analysis
- Title not available (Why is that?)
- Formal analysis of piecewise affine systems through formula-guided refinement
- Before and after vacuity
- Modelling timed reactive systems from natural-language requirements
- Model checking of biological systems
- Modeling and querying biomolecular interaction networks
- Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams
- Verifying the IEEE 1394 fireWire tree identify protocol with SMV
- Symbolic CTL model checking of asynchronous systems using constrained saturation
- Acacia+
- CITP
- CTL-RP
- MinGW
- P-Lingua
- BINSEC/SE
- CAESAR
- PyCUDD
- VCS
- Dynamic Architectures
- FACTum
- Lorel
- C2M
- MSVL
- ASSA-PBN
- CuSNP
- Jass
- PQL
- UMC4M
- JBotSim
- AdamMC
- zUpdate
- Tools and Algorithms for the Construction and Analysis of Systems
- Specifying norm-governed computational societies
- PTrie
- GNA
- Architectural_Design_Patterns
- CompoSAT
- ASMETA
- PuRSUE
- DynAlloy
- FaSTrack
- EPFL
- Papyrus-RT
- VIS
- Time-budgeting: a component based development methodology for real-time embedded systems
- Proof-based verification approaches for dynamic properties: application to the information system domain
- On the verification of very expressive temporal properties of non-terminating Golog programs
- Theory and Applications of Satisfiability Testing
- Verification of Boolean programs with unbounded thread creation
- Title not available (Why is that?)
- Modeling and analysis of gene regulatory networks
- Deductive verification of simple foraging robotic behaviours
- Compressing BMC encodings with QBF
- Verification, Model Checking, and Abstract Interpretation
- Computation Tree Regular Logic for Genetic Regulatory Networks
- An overview of the mCRL2 toolset and its recent advances
- Title not available (Why is that?)
- A compiler for MSVL and its applications
- On the expressivity and complexity of quantitative branching-time temporal logics
- VCS: a verifier for component-based systems
- Translating Xd-C programs to MSVL programs
- NuMDG: a new tool for multiway decision graphs construction
- SPOT
- Alcoa
- DESUMA
- GIDDES
- MCK
- CBMC
- BEEM
This page was built for software: NuSMV
