Skip to content
a model extractor, to automatically extract Spin verification models from multi-threaded C code
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.
Examples initial release Dec 21, 2018
Src lgtm fixes Mar 5, 2019 initial release Dec 21, 2018
makefile makefile Mar 2, 2019


a model extractor for the Spin model checker

Modex can be used to mechanically extract verification models from implementation level C code. first developed at Bell Labs starting in 1998, and released as open-source in 2002. The model extractor is guided by a user-defined test-harness, specified in a separate file with extension ".prx". The format used in test-harness files is documented in the Manual.

For details on the theoretical background for the tool, and its installation and use, see for instance

You can’t perform that action at this time.