opaal

opaal is a distributed/parallel (discrete time) model checker for networks of timed automata implemented in Python using MPI. opaal is designed to be easily extendible, such that different approaches can be prototyped quickly.

opaal come to live a late night at the Department of Computer Science at Aalborg University, where Mads Chr. Olesen and Kenneth Yrke Jørgensen after extensive and long discussions about how difficult it would be to implement a parallel/distributed model checker that was easy to experiment with.

Today opaal is an official project at Department of Computer Science at Aalborg University where development is a part of active research projects. 

If you want to know more about opaal please see our webpage at: www.opaal-modelchecker.com or opaal launchpad page.