Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-75867-9_30 | EUROCAST |
Keywords | Field | DocType |
particular property,different proof assistant,program property,video-on-demand server,theorem provers,different theorem provers,selected scenario,real-world application,case study,proof assistant,theorem prover | Theorem provers,Computer-assisted proof,Programming language,Computer science,Interval Sequence,Software,Systems development life cycle,Proof assistant | Conference |
Volume | ISSN | ISBN |
4739 | 0302-9743 | 3-540-75866-6 |
Citations | PageRank | References |
0 | 0.34 | 4 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| J. Santiago Jorge | 1 | 6 | 3.31 |
| Víctor M. Gulias | 2 | 30 | 6.06 |
| Laura M. Castro | 3 | 50 | 10.39 |