Opened 12 years ago

Last modified 12 years ago

#69 new proposed-project

Implement a model checker

Reported by: asiekiel Owned by: none
Priority: Keywords:
Cc: Difficulty: unknown
Mentor: not-accepted Topic: misc

Description (last modified by asiekiel@…)

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 <asiekiel@…>

Change History (1)

comment:1 Changed 12 years ago by asiekiel@…

Description: modified (diff)

Added interested student/mentors part.

Note: See TracTickets for help on using tickets.