Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server
2008
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.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
10
References
0
Citations
NaN
KQI