Tools for Logic Programming

The declarative nature of logic programming simplifies the task of checking that a program is correct. In fact, some forms of correctness, such as termination, or deadlock freedom, can be verified, at least to some extent, without actually running the program. This PhD studentship will consider the issue of determinism detection. Predicates are often intended to be deterministic, but are actually non-deterministic in subtle ways, which can impede the performance of a program. The PhD studentship will develop tools for checking determinism in logic and constraint logic programs, exploring the connections that have recently emerged with termination checking.