Thesis Topic Details

Topic ID:
3428
Title:
Refactoring Machine-checked Proofs
Supervisor:
Rafal Kolanski
Research Area:
Formal Methods, Software Engineering
Associated Staff
Assessor:
June Andronick
Topic Details
Status:
Active
Type:
R & D
Programs:
CS CE BIOM BINF SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
COMP4161
Description:
This thesis project is about further developing an automated refactoring tool for mathematical proofs that are machine-checked in the theorem prover Isabelle/HOL.

The existing version of the tool is written in Scala, implements a simple "rename" refactor and beginnings of a "move theorem" refactor.

The objective of this thesis is to develop a scalable "move theorem" refactor that is fully automated and that can be run unsupervised with minimal user hints on a repository of proofs that span over 400,000 lines of Isabelle proof scripts. The "move theorem" refactor should be able to compute the highest useful point in a theory graph for the destination of a theorem and it should be able to deal with global state exhibited by the prover, such as simplification sets. It should also be able to deal gracefully with local contexts and locales, ideally with the ability to transfer a theorem out of a local context automatically without adding unnecessary assumptions to the theorem.

If this refactor is implemented successfully, the thesis should investigate which other useful refactors can be implemented in this tool.
Comments:
The thesis is part of NICTA's work on formally verified software in the software systems research group.
Past Student Reports
  Avi Joshua KNOLL in s2, 2013
Refactoring Machine-checked Proofs
 

Download report from the CSE Thesis Report Library

NOTE: only current CSE students can login to view and select reports to download.