Skip to main content
Department of Information Technology

opaal: A Prototype Model Checker


Mads Christian Olesen
PhD student in the Distributed and Embedded Systems group at the Department of Computer Science, Aalborg University

Date and Time

Thursday, June 16th, 2011 at 13:30


Polacksbacken, room 1146


We present a new open source model checker, opaal, for automatic verification of models using lattice automata. Lattice automata allow the users to incorporate abstractions of a model into the model itself. This provides an efficient verification procedure, while giving the user fine-grained control of the level of abstraction. Lattice automata generalise, among others, timed automata.

The opaal engine supports a subset of the UPPAAL timed automata language extended with lattice features, and is designed to allow for rapid prototyping while being easy to learn and sufficiently fast. For these reasons it is implemented in Python.

Currently, opaal is still a work in progress; it has nevertheless been used successfully by students to try out a new data structure for clocks.


Kim Guldstrand Larsen, René Rydhof Hansen

Back to the seminar page

Updated  2011-05-18 11:03:31 by Frédéric Haziza.