Starting Date: June 2022
Prerequisites: Good mathematical background; Functional programming skills; Interest in verification.
Will results be assigned to University: No
Cyclic proofs are a technique for proving properties inductively, or proving properties about inductively defined objects or processes. They can be used to prove logical statements, or to verify recursive programs.
The Cyclist tool [1] has been developed as an automatic verification tool based on cyclic proofs. It can prove termination and verify temporal properties of simple programs with recursive procedures in a C-like language (with explicit pointer manipulation).
Currently, users have to write quite complex specifications for their programs, which includes describing how termination measures are changed by procedures. In recent research [2], we have started developing a technique for automatically computing these changes. This would make it easier for users to specify and verify correctness of their programs, by getting the computer to do more automatically.
This project would involve investigating how the research can be implemented in the Cyclist tool. The overall aim is to make Cyclist more user-friendly, and to increase its power to automatically verify programs.
[1] http://www.cyclist-prover.org/
[2] Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent. Reuben N. S. Rowe and James Brotherston. https://doi.org/10.1007/978-3-319-66902-1_18