Verification of program properties using different theorem provers: a case study
2007
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.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
14
References
0
Citations
NaN
KQI