Model checking has been conceived as a powerful tool for hardware, software and protocol verification, which has its main
application fields in the development of hi-tech and safety-critical systems. We present here a completely novel application
in the field of university administration processes, in which model checking is applied to the verification of the coherence
of syllabi and to the automated synthesis/simulation of correct student careers under given requirements.
The first and the third author are part of the SS2 project team. The other team members provided feedback on the formalization.
Alessandro Cimatti, Marco Roveri and Paolo Traverso from ITC-IRST provided help on Symbolic Model Checking.