Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server

详细信息    查看全文

• 作者：J. Santiago Jorge ; Victor M. Gulias ; Laura M. Castro
• 关键词：Formal methods ; software verification ; theorem provers ; functional programming ; real ; world applications
• 刊名：Lecture Notes in Computer Science
• 出版年：2008
• 出版时间：2008
• 年：2008
• 卷：5144
• 期：1
• 页码：296-299
• 全文大小：238.9 KB

文摘

In this paper we describe our experiences applying formal software verification in a real-world distributed Video-on-Demand server. As the application of formal methods to large systems is extremely difficult, relevant properties of a particular subsystem have been identified and then verified separately. Conclusions on the whole system can be drawn later. The development consists of two parts: first, the definition of the algorithm in the coq proof assistant; second, codification of the theorems with the help of some new tactics derived from the abstraction of verification patterns common to different proofs.