A computer program, such as Microsoft Word, requires regular updates to fix bugs. Detecting and fixing problems manually is a lot of work: time-consuming and costly. For this reason, systems are emerging that allow the checks to be done automatically, without the need for a programmer to intervene.
Computer science is a broad field with two poles: the theoretical and the practical. Refinement types aim to merge these two poles and allow conventional programming to enjoy some advantages. They provide an attractive, automated form of formal verification used to check that real-world applications are correct, such as that a web application does not leak private user information. However, currently the refinement types do not provide any mathematical proof that verifies the absence of private information leakage.
The project, led by Niki Vazou, is designing a robust and practical system of refinement types to make program development faster, more secure and error-free.
In addition, CRETE aims to make formal verification so attractive that it can be used as an aid in programming courses and to promote verified programming as the de facto way to teach programming.
