NUSMV: a new symbolic model checker

By A. Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri. International Journal on Software Tools for Technology Transfer (STTT), 2000

863 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/ef76123b4f149a61f99d9940c84e806612e4e6a2

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

1. Joost-Pieter Katoen
2. Paolo Traverso
3. Marco Pistore
4. Christel Baier
5. Corina S. Pasareanu
6. Andreas Podelski
7. Sarfraz Khurshid
8. Somesh Jha

In Software

1. Joost-Pieter Katoen
2. Paolo Traverso
3. Marco Pistore
4. Christel Baier
5. Corina S. Pasareanu
6. Andreas Podelski
7. Sarfraz Khurshid
8. Willem Visser

Citations in the corpus

• Weak, strong, and strong cyclic planning via symbolic model checking (2003, methodology): “In its internals, MBP inherits from NUSMV the use of CUDD [62], one of the best BDD packages available.”
• Automated composition of Web services via planning in asynchronous domains (2005, methodology): “SMV is the native language used in modelchecking systems such as NuSMV [27].”
• The tropos software development methodology: processes, models and diagrams (2002, background): “Moreover, such speci cations can be simulated using model checking technology for validation purposes [13, 8].”
• Planning as Model Checking in Hybrid Domains (2014, methodology): “We remark that our current implementation does not yet extract these plans, but this step is purely technical and efficiently implementable (essentially a call to an SMT solver).”
• Counterexample-guided abstraction refinement for symbolic model checking (2003, methodology): “We have implemented a prototype tool aSMV based on NuSMV [Cimatti et al. 1998] and applied it to a number of benchmark designs.”
• Counterexample-Guided Abstraction Refinement (2000, methodology): “Although our current implementation is based on NuSMV, it is in principle not limited to the input language of SMV and can be applied to other languages.”
• Principles of model checking (2008, methodology): “LTL model checking using a tableau construction is supported by NuSMV [83].”
• Model-Checking Algorithms for Continuous-Time Markov Chains (2002, methodology): “With appropriate tools such as SMV [22], SPIN [45], and Mur' [31], systems of several millions of states have been analyzed.”
• Generalized Symbolic Execution for Model Checking and Testing (2003, methodology): “Other projects, such as Bandera [6], translate Java programs into the input language of SPIN [12] and NuSMV [4].”