New York
LondonBeijing
Certifying Properties of Programs Using Theorem provers

Certifying Properties of Programs Using Theorem provers

J. Santiago Jorge (University of A Coruna, Spain), Victor M. Gulias (University of A Coruna, Spain), and David Cabrero (University of A Coruna, Spain)
Copyright: © 2007 |Pages: 50
DOI: 10.4018/978-1-59140-851-2.ch010
OnDemand:
(Individual Chapters)
Available
$37.50
Current Special Offers
No Current Special Offers
TOTAL SAVINGS: $37.50

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.

Complete Chapter List

Search this Book:
Reset