Overview
Topic status: We're looking for students to study this topic.
Project situated at Brisbane SUN Microsystems laboratory
Model checking is a technique based on temporal logic that can be used to verify properties about a system. In this project, the aim is to use the SPIN model checker as part of Parfait to find bugs, as well as use the model checker to determine if a particular bug reported by Parfait is a false positive (as the model checker can find a path that exposes the bug or lack of bug). Code to be written in this project is in C++.
- Study level
- Honours
- Supervisors
- QUT External Cristina Cifuentes (SUN Microsystems Laboratory)
- Organisational unit
Science and Engineering Faculty
- Research area
- Contact
- Please contact the supervisor.
Associate Professor Shlomo Geva
