, , , ,

To link papers to this page, give a list of papers ids in the References field. (Same mechanism as the Research Themes pages)

Under Construction

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.

If you are interested in obtaining a copy of the Milestones model checker. Do not hesitate to contact Josť Vander Meulen.

README : Milestones-README

Current version :

If you want to add an historic, giving older versions, etc, you can do it here.

Josť Vander Meulen

Related Publications: