Paper Info
Title
Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server
Abstract
In this paper we describe our experiences applying formal software verification in a real-world distributed Video-on-Demandserver. 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 coqproof assistant; second, codification of the theorems with the help of some new tactics derived from the abstraction of verification patterns common to different proofs.
Year
DOI
Venue
2008
10.1007/978-3-540-85110-3_25
AISC/MKM/Calculemus
Keywords
Field
DocType
relevant property,verification pattern,formal software verification,formal method,prove properties,particular subsystem,different proof,cache level,whole system,large system,coqproof assistant,functional video-on-demand server,new tactic,theorem prover,software verification
Abstraction,Programming language,Functional programming,Computer science,Cache,Theoretical computer science,Mathematical proof,Formal methods,Software verification,Formal verification,Proof assistant
Conference
Volume
ISSN
Citations 
5144
0302-9743
0
PageRank 
References 
Authors
0.34
6
3
Name
Order
Citations
PageRank
J. Santiago Jorge163.31
Víctor M. Gulias2306.06
Laura M. Castro35010.39