NuSMV 2: An OpenSource Tool for Symbolic Model Checking

1,709 citations recorded by the source corpus.

How researchers see this paper

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

Abstractions for network update (2012, methodology): “We illustrate the utility of this idea concretely by deploying the NuSMV model checker [13] to verify invariance of a variety of important trace properties that arise in practice.”
Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2 (2017, methodology): “Proving the correctness of the above countermeasure is straightforward: we modeled the modified state machine in NuSMV [23], and used this model to prove that two key installations are always separated by the generation of a fresh PTK.”
Bounded model checking (2003, background): “NuSMV [10]), and a number of advances have been achieved in several directions, which we briefly describe now.”
Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in Escherichia coli (2005, positive): “In order to combine our qualitative simulator with modelchecking tools, we have integrated export functionalities in the new version of GNA, allowing the user to generate text files describing the qualitative transition system in the format accepted by two widely used model checkers, NuSMV ( Cimatti”
The nuXmv Symbolic Model Checker (2014, background): “NUXMV extends the NUSMV [1] architecture as described here after.”