Anders Schlichtkrull PhD project: Formalization of Algorithms and Logical inference Systems in Proof Assistants

Abstract

The purpose of the project is to use proof assistants to prove that algorithms and logical inference systems work correctly, i.e. as intended. For instance, a proof assistant could be used to prove that an aircraft alerting algorithm indeed does alert aircrafts if they get too close. To prove something, means to argue rigorously that it is true. Proof assistants are computer programs that can read such proofs, and check that they are correct. The proofs for proof assistants have to be written in special proof languages which are similar to programming languages, and the proof assistant ensures that all the arguments used in the proofs are valid. The proof assistant can also conduct parts of the proofs automatically.

Proof assistants can be applied to verify algorithms and logical inference systems, and this is especially advantageous since it has real world implications on our society that they work correctly. They are used in computer programs, mobile apps, web applications, etc. For instance, logical inference systems are used in description logic which has applications in medical science, software engineering, and the semantic web. Algorithms are used for instance to sort rows in a spreadsheet computer program or perform a search on the internet. Proof assistants have already been used to prove correct an operating system which can be used in smartphones, the division algorithm of the AMD5K86 microprocessor, and an aircraft alerting algorithm.

Contact

Jørgen Villadsen
Associate Professor
DTU Compute
+45 45 25 37 33

Contact

Thomas Bolander
Associate Professor
DTU Compute
+45 45 25 37 15

Contact

Anders Schlichtkrull
PhD student
DTU Compute
+45 45 25 34 62