Interest in formal logic; knowledge of OCaml, or another functional programming language, or the ability and willingness to learn.
Propositional Dynamic Logic (PDL)  is a logic in which abstract properties about the behaviour of programs can be expressed, in a very general way. Because of its generality it is suitable for checking the behaviour or a wide range of programs and systems, via model checking.
PDL is what is known as a modal logic, meaning that logical formulas are subject to modalities that, in this context, describe the actions of programs. If a modality is applied to a formula, the intended meaning is that the property expressed by the formula will hold after the action of some program (indicated by the modality) is performed.
For example, the formula (x > 4) ⟶ [x++](x > 5) expresses the simple fact that, if the variable
x holds a value greater than 4, then after executing the code
x++ incrementing the variable, it will hold a value greater than 5.
Although algorithms already exist for deciding the validity of statements in PDL, recent research  has developed a cyclic proof system for PDL that can also be used as the basis for deciding validity, through a process of proof search. The aim of this project would be to implement the proof system within the Cyclist automatic theorem proving framework . Cyclist is a framework, written in the OCaml functional programming language , for generating automatic provers from a definition of a cyclic proof system.
Once the cyclic prover is produced for PDL, we would then test it against implementations of the existing algorithms.
 Simon Docherty, Reuben N. S. Rowe: A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic. TABLEAUX 2019