Case Studies


Random Swap

Original program in UPC
Revised program in UPC




Single lane Bridge

Original program in Promela
Revised program in Java (CorrectBridge.java, NewBlueCar.java, NewRedcar.java)


Barrier Synchronization


Original program in Promela
Revised program in Promela



Token Ring


Original program in Promela
Revised program in Promela


Two Single Lane Bridges


Original program in Promela
Revised program in Promela


Softwar Design Laboratory at MichiganTech


Towards the Model Checking of the Partitioned Global Address Space (PGAS) Applications