Name
Abstract | ||
|---|---|---|
This paper describes the nuXmv symbolic model checker for finite- and infinite-state synchronous transition systems. nuXmv is the evolution of the nuXmv open source model checker. It builds on and extends nuXmv along two main directions. For finite-state systems it complements the basic verification techniques of nuXmv with state-of-the-art verification algorithms. For infinite-state systems, it extends the nuXmv language with new data types, namely Integers and Reals, and it provides advanced SMT-based model checking techniques. Besides extended functionalities, nuXmv has been optimized in terms of performance to be competitive with the state of the art. nuXmv has been used in several industrial projects as verification back-end, and it is the basis for several extensions to cope with requirements analysis, contract based design, model checking of hybrid systems, safety assessment, and software model checking. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/978-3-319-08867-9_22 | CAV |
Field | DocType | Volume |
Integer,Programming language,Model checking,Predicate abstraction,Computer science,Algorithm,Requirements analysis,Source model,Theoretical computer science,Data type,Hybrid system,Symbolic trajectory evaluation | Conference | 8559 |
ISSN | Citations | PageRank |
0302-9743 | 34 | 1.42 |
References | Authors | |
33 | 9 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Roberto Cavada | 1 | 148 | 7.87 |
| Alessandro Cimatti | 2 | 5064 | 323.15 |
| Michele Dorigatti | 3 | 71 | 2.91 |
| Alberto Griggio | 4 | 624 | 36.37 |
| Alessandro Mariotti | 5 | 34 | 1.42 |
| Andrea Micheli | 6 | 190 | 14.08 |
| Sergio Mover | 7 | 218 | 15.23 |
| Marco Roveri | 8 | 1678 | 96.70 |
| Stefano Tonetta | 9 | 573 | 41.61 |