This is the Software Description Document (SDD) for the C API to nuXmv, a symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.

The document is composed of the following sections:

Data Structures shows a sorted list of data types.
Topics follows the structure of the header file nuxmv.h and presents the data types and functions available to the programmer.
Unimplemented Functions shows a list of functions which are available through the API but that will be available in future releases.

Author: Fondazione Bruno Kessler <https://www.fbk.eu/>

Date: 2026-04-02

Copyright: You may study, copy, compile and execute this Software only for academic, non-commercial research purposes, subject to the restrictions in the LICENSE.txt that accompanies the Software.