The Model Checking in Education (MCiE) Project
The Model Checking in Education (MCiE) Project was started in January 2004
in conjunction with a course
on model checking at Paderborn University.
The idea was to supplement the course with an implementation
of the theoretical concepts presented in this course. This
implementation should provide some insight into the details
of a model checker that could not be addressed in the lectures.
Currently,
the implementation provides an ROBDD library and a simple CTL
model checker. Eventually, all concepts discussed during the
course on model checking will be implemented.
The focus of the MCiE project is on a clean implementation which
allows a safe use (even when used or modified by students) and
easy extensibility. Since efficiency was not its main issue, we
have chosen Java as the implementation language and avoided some
common hacks for improving efficiency.
Licence
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.
MCiE 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.
Contact
For more information or bug reports, contact
Ekkart Kindler,
kindler@upb.de.
Documentation and downloads (Vers. 0.1.4)