Student research opportunities
Proving Safety Properties
Project Code: CECS_1160
This project is available at the following levels:
Honours, Summer Scholar, Masters
Keywords:
Model Checking, Automated Reasoning
Supervisor:
Dr Peter BaumgartnerOutline:
Fitzroy is a model-checker for the logic CTL* over fragments of first-order logic. Unlike most other systems, it supports modelling of states with a rich structure using lists, arrays and records and first-order logic. Fitzroy is implemented in Scala.
Goals of this project
A safety property says that a bad state can never be reached, for example that a certain program variable is never set to a particular value. Fitzroy currently employs a technique called K-Induction for proving safety properties. Alternatives to that do exist, based on interpolation or on overapproximation, as popularized by the IC3 system. Can we take advantage of these more modern technologies in Fitzroy?
Requirements/Prerequisites
Working knowldge of Scala (or Java)
Student Gain
Becoming aquainted with and contributing to the state of the art in automated theorem proving and model checking
Background Literature
See paper below
