opaal model checker

opaal is a model checker with the design goals of enabling rapid prototyping, being easy to learn and being sufficiently fast. It should be the first tool used when wanting to try out a model checking concept, therefore it needs to be open source. It should be so easy to learn that a group of undergraduate students can implement something useful with it in one semester. This requires readability, good overview and loose coupling. It should be sufficiently fast, by implementing the low-hanging optimisation fruit - gold plating is forbidden!

The opaal manifest

The design criteria for opaal is:

  1. Rapid prototyping
  2. Easy to learn
  3. 80-20 rule for optimisations


1. Rapid prototyping

Try out concepts quickly
Before doing more time-consuming, optimised implementation
Open Source

2. Easy to learn

A group of 5th semester students should be able to implement
something in a project
Readability, overview, loose coupling

3. Implement the 20% of the optimisations that give 80% of the speedup

No gold plating
Sufficiently fast
We learn as we go

Site under construction

Please see https://launchpad.net/opaal for even less information!