Description: |
CEGAR means Counter-Example guided Abstraction Refinement and refers to one of the most useful techniques to extend the range of problems amenable to model checking. More often than not, real systems and real properties are too complex to be checked against each other automatically in a brute-force manner. It is however possible to check safe abstraction of real systems against mathcing abstraction of properties in a way that guarantees that if the abstraction has the abstracted property then the real system complies with the real property (but typically not vice versa). While a number of industrial strength model checkers are available under open source licenses, there is a distinct lack of a CEGAR testbed in the open that allows researchers to evaluate new abstractions against test suites of systems and properties. The aim of this thesis project is to develop a prototype CEGAR tool. Haskell is suggested as the programming language in order to speed up development and to exploit local knowledge. |
