New API and bug fixes
The Formal Methods for System and Software Research Unit (FM) is proud to release the latest version of nuXmv, our symbolic model checker for the analysis of synchronous finite-state and infinite-state systems, for Linux, MacOS and (coming soon) Windows.
The major addition to the project consists of a C99-compliant Application Programming Interface (API) which is meant to facilitate the integration of the model checker with other projects. The release ships with a Tutorial, a working example, and an API reference. A Python wrapper is in the pipeline, too.
Other notable additions are:
- rlive as algorithm option in
check_ltlspec_ic3for finite-state systems only - an option to select a property by name in
write_vmt_model.
Minor changes bring fixes to VMT model reading, param synthesis with properties via command line, and documentation.
Useful links:
- nuXmv home page
- nuXmv download page
- API Tutorial and Getting Started page
- API Software Description Document