Abstract
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. © 2008 Springer-Verlag Berlin Heidelberg.
Author supplied keywords
Cite
CITATION STYLE
Jorge, J. S., Gulias, V. M., & Castro, L. M. (2008). Using Coq to prove properties of the cache level of a functional video-on-demand server. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5144 LNAI, pp. 296–299). https://doi.org/10.1007/978-3-540-85110-3_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
