Praktikum Compiler Construction (Compilerbau) 2007

Due to lack of interest the Praktikum is cancelled.
Das Praktikum entfällt wegen mangeldem Interesse.

Contents

PRISM is a probabilistic model checker, a tool for formal modelling and analysis of probabilistic systems. It supports three types of probabilistic models:

  • discrete-time Markov chains (DTMCs)
  • continuous-time Markov chains (CTMCs)
  • Markov decision processes (MDPs)

Models are described using the PRISM language, a simple, state-based language.

The purpose of this project is to implement a tool that accepts a program in the Prism input language (for CTMCs and DTMCs) and produces the underlying Markov chain in the simple text format .tra, .lab, .rew, .rewi supported by the MRMC model checker. The project should be carried out in either C or C++. We will provide some of the internal data structures.

The best implementation will be integrated into the MRMC tool.

Schedule

to be announced

Requirements

  • Vordiplom Informatik
  • Lectures Compiler Construction or PaCo, maybe also Advanced Model Checking
  • Programming experience in C or C++

Links / Literature

CVS

We will use the versioning system CVS. You should accomodate yourself with it before the start of the project.

Contact

Stefan Rieger
Ivan Zapreev