id,summary,reporter,owner,description,type,status,priority,resolution,keywords,cc,topic,difficulty,mentor
69,Implement a model checker,asiekiel,none,"[http://manta.univ.gda.pl/~asiekiel/jhypernets jhypernets] is a simulator of a formal model of mobile computations
called ""Petri hypernets"", with a core implemented in Haskell. The model
supports model checking (automatic checking of satisfiability of logical
formulas). At the moment there is a very simple model checker
implemented in Haskell which is too slow for using it for non-trivial
models. The idea is to implement a fast model checker in Haskell using
Symbolic Model Checking. It requires implementing or creating bindings
to a BDD (Binary Decision Diagrams) library, implementing the model
checker itself (which is a non-standard one) and possibly strong
profiling of code.

The project could be a proof of a hypothesis ""Haskell is a great
tool for implementing systems specified formally"". The hypothesis is
partially proved at the moment (Haskell component is a very successful
part of the project), but creating a model checker is a very
implementation-speed-sensitive and we do not know whether we can have
the high-levelness of Haskell and speed of imperative languages at the
same time (in the domain of model checkers).

== Interested Mentors ==
  * ?

== Interested Students ==
  * Artur Siekielski <[mailto:asiekiel@manta.univ.gda.pl]>",proposed-project,new,,,,,misc,unknown,not-accepted