Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
The nuXmv Symbolic Model Checker
verfasst von : Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta
Erschienen in: Computer Aided Verification
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.