Starting Date: July 2026
Prerequisites: Strong programming skills (ideally OCaml or C++); strong skills in algorithms; analytical thinking
Will results be assigned to University: No
The Infinite Descent property underpins two very important applications in program verification: termination of programs [1,2], on the one hand, and correctness of cyclic proofs of formulas or properties [3], on the other. In both cases, the object of interest (i.e. a program or a proof) is converted into an abstract form for which the Infinite Descent property can be checked.
The abstract form used for checking Infinite Descent is called a sloped graph. This is a standard directed graph (i.e. edges connecting nodes), where each node contains a number of positions and the edges are labelled with a relation describing how the positions are related via (strictly) decreasing slopes.
In recent work [3], we have collected a large number of these sloped graphs from the Cyclist theorem prover [4]. This provides a very useful benchmarking suite for algorithms for checking the Infinite Descent property (some of which we have developed [3,5]). However, many of the sloped graphs we collected are isomorphic, meaning that although the concrete representations are different (e.g. the nodes and positions are given different names, the edges are specified in a different order, etc.), they in fact represent the same underlying sloped graph.
The objective of this project will be to implement an algorithm that can decide when two sloped graph representations are isomorphic. This is important to know in order the evaluate how broad the benchmarking suite actually is, and how effective it is at evaluating the performance of the different algorithms, since the algorithms should perform similarly on isomorphic sloped graphs.
The question of sloped graph isomorphism is an extension of the well known standard graph isomorphism problem, which is a very important (and hard) problem in Computer Science. There are existing (very clever) algorithms for this problem (e.g. [6,7]), but they will need to be adapted to our specific setting of sloped graphs. Alternatively, you can develop your own algorithm.
Ideally, you would implement this as part of the Cyclist theorem prover framework, and so use either OCaml. As part of the project, you can also write code to compute data about different metrics of the sloped graphs. This will also be useful in categorising the graphs in the benchmark suite, and lead to more sophisticated ways to compare the performance of algorithms deciding the Infinite Descent property.
References
[1] https://en.wikipedia.org/wiki/Size-change_termination_principle
[2] Chin Soon Lee, Neil D. Jones, Amir M. Ben-Amram. The size-change principle for program termination. POPL 2001: 81-92. https://doi.org/10.1145/360204.360210
[3] Liron Cohen, Reuben N. S. Rowe, Matan Shaked. Cyclone: A Heterogeneous Tool for Verifying Infinite Descent. TACAS (1) 2025: 336-354. https://doi.org/10.1007/978-3-031-90643-5_18
[4] http://www.cyclist-prover.org/
[5] Liron Cohen, Adham Jabarin, Andrei Popescu, Reuben N. S. Rowe. The Complex(ity) Landscape of Checking Infinite Descent. Proc. ACM Program. Lang. 8(POPL): 1352-1384 (2024). https://doi.org/10.1145/3632888
[6] https://www.quantamagazine.org/algorithm-solves-graph-isomorphism-in-record-time-20151214/
[7] Martin Grohe and Pascal Schweitzer. The graph isomorphism problem. Commun. ACM 63, 11 (November 2020), 128–134. https://doi.org/10.1145/3372123
[8] https://www.ocaml.org/