The purpose of the Model Checking in Education (MCiE) project is to demonstrate the implementation of a symbolic model checker based on ROBDDs. It was implemented by Ekkart Kindler as supplementary material for the students of the course on model checking in the winter term 2003/04 at Paderborn University.

Since this first course, MCiE has been extended and improved when used in other projects and during the course "Advanced Topics on Software Engineering" at Denmark's Technical University.

Since the main purpose of this application was educational, it is not particularly tuned to efficiency, but for a clear structure and a safe usability of the libraries. At some places in the code, comments indicate what could be done for improving efficiency - apart from using a compiled programming language such as C instead of Java.

Release notes


Copyright (C) 2004, 2006 Ekkart Kindler, University of Paderborn, kindler@upb.de

Copyright (C) 2009, 2010 Ekkart Kindler, Denmark's Technical University (DTU), eki@imm.dtu.dk

The MCiE project is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; version 2 of the License.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA @author Ekkart Kindler @version 0.3.7