Verify algorithms' properties with the MSR(C) prototype

MSR(C) is a tool to model-check infinite state systems, extending Petri Nets ideas.
The goal of this project is to verify properties of given algorithms for self-organising networks.
We will explore the main aspect of the MSR(C) specification and with the help of some example we want to test this tool to expose strengths and weaknesses and propose alternatives if necessary.

• Msr(C)
• Model Checking in CLP
• PFS Prototype
• PFS Paper