Verification of Program Properties Using Different Theorem Provers: A Case Study

摘要

This paper explores the use of theorem provers to certify particular properties of software. Two different proof assistants are used to illustrate the method: Coq and Pvs. By comparing two theorem provers, conclusions about their suitability can be stated. The selected scenario is part of a real-world application: a distributed Video-on-Demand server. The development consists on two steps: first, the definition of a model of the algorithm to be studied in the proof assistants; second, the development and proving of the theorems.