The following pages link to NuSMV (Q16316):
Displayed 50 items.
- \texttt{VeriSIMPL 2}: an open-source software for the verification of max-plus-linear systems (Q262437) (← links)
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (Q264193) (← links)
- Extracting unsatisfiable cores for LTL via temporal resolution (Q266863) (← links)
- Analysing sanity of requirements for avionics systems (Q282095) (← links)
- Verification of \(\mathrm{EB}^3\) specifications using CADP (Q282110) (← links)
- Bounded situation calculus action theories (Q286407) (← links)
- Modelling timed reactive systems from natural-language requirements (Q315301) (← links)
- Bounded model checking of ETL cooperating with finite and looping automata connectives (Q364388) (← links)
- An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints (Q414857) (← links)
- SAT-solving in CSP trace refinement (Q436423) (← links)
- A decidability result for the model checking of infinite-state systems (Q438572) (← links)
- Interrupt timed automata: verification and expressiveness (Q453513) (← links)
- Symbolic bounded synthesis (Q453535) (← links)
- An analytic tableau calculus for a temporalised belief logic (Q456722) (← links)
- Linear temporal logic symbolic model checking (Q465680) (← links)
- Model checking RAISE applicative specifications (Q470000) (← links)
- Complexity of fixed-size bit-vector logics (Q504997) (← links)
- Enhancing unsatisfiable cores for LTL with information on temporal relevance (Q507378) (← links)
- Component-wise incremental LTL model checking (Q510894) (← links)
- Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems (Q528185) (← links)
- CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks (Q548484) (← links)
- A formalisation of violation, error recovery, and enforcement in the bit transmission problem (Q598545) (← links)
- MAVEN: Modular aspect verification and interference analysis (Q609017) (← links)
- Bisimulation conversion and verification procedure for goal-based control systems (Q633304) (← links)
- Verification of consensus algorithms using satisfiability solving (Q658669) (← links)
- Synthesis of obfuscation policies to ensure privacy and utility (Q682359) (← links)
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability (Q729813) (← links)
- Time-budgeting: a component based development methodology for real-time embedded systems (Q736795) (← links)
- Program repair without regret (Q746769) (← links)
- Game-theoretic simulation checking tool (Q764005) (← links)
- Using formal verification to evaluate the execution time of Spark applications (Q782497) (← links)
- Weak, strong, and strong cyclic planning via symbolic model checking (Q814470) (← links)
- Conformant planning via symbolic model checking and heuristic search (Q814631) (← links)
- Translating Java for multiple model checkers: The Bandera back-end (Q816196) (← links)
- Timed hyperproperties (Q821560) (← links)
- Not all bugs are created equal, but robust reachability can tell the difference (Q832220) (← links)
- Model checking \(\omega \)-regular properties with decoupled search (Q832281) (← links)
- Action language verifier: An infinite-state model checker for reactive software specifications (Q845244) (← links)
- AutoSyn: A new approach to automated synthesis of composite web services with correctness guarantee (Q848309) (← links)
- Verifying data refinements using a model checker (Q851129) (← links)
- The formal-CAFE methodology and model checking patterns in the specification of e-commerce systems (Q862581) (← links)
- Data structures for symbolic multi-valued model-checking (Q862857) (← links)
- From NuSMV to SPIN: Experiences with model checking flight guidance systems (Q883136) (← links)
- Early verification and validation of mission critical systems (Q883137) (← links)
- HRELTL: a temporal logic for hybrid systems (Q897648) (← links)
- Agent planning programs (Q899440) (← links)
- Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning (Q934706) (← links)
- Automatic symbolic compositional verification by learning assumptions (Q934713) (← links)
- On regular temporal logics with past (Q977176) (← links)
- Test generation from P systems using model checking (Q987969) (← links)