Tools
Milestones
The Milestones model checker combines symbolic techniques and POR. Its goal is to verify temporal properties on concurrents systems.
On such a system, Milestones allows to check the absence of deadlock, LTL properties, and CTL properties.
Milestones is able to translate a model into an equivalent Spin model or NuSMV model.
README : Milestones-README
Current version : Milestones.zip
- Contributor(s)
- José Vander Meulen
Related Publications:
- Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction. José Vander Meulen, Charles Pecheur. NASA FORMAL METHODS 2011.