Certifying Properties of Programs Using Theorem provers

Abstract

Proving the correctness of a program, even the simplest one, is a complex and expensive task; but, at the same time, it is one of the most important activities for a software engineer. In this chapter, we explore the use of theorem provers to certify properties of software; in particular, two different proof-assistants are used to illustrate the method: Coq and PVS. Starting with a simple pedagogic example, a sort algorithm, we finally reproduce the same approach in a more realistic scenario, a model of a block-allocation algorithm for a video-on-demand server.