Skip to Main content Skip to Navigation
Conference papers

You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3

Abstract : We report on a solution we designed for the VerifyThis Collaborative Long Term Challenge 2019. We used the Why3 verification framework to design, from scratch, a simple but running prototype implementation of a PGP key server. We exploit the ability of Why3 to extract OCaml code from verified WhyML code so as to produce code that can be compiled into an executable. Our prototype is made of a combination of unverified handwritten OCaml code and of WhyML code whose functional behaviour is formally specified and proven correct.
Document type :
Conference papers
Complete list of metadatas

Cited literature [6 references]  Display  Hide  Download

https://hal.inria.fr/hal-03002187
Contributor : Claude Marché <>
Submitted on : Thursday, November 12, 2020 - 4:55:11 PM
Last modification on : Sunday, November 15, 2020 - 3:26:28 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03002187, version 1

Collections

Citation

Diego Diverio, Cláudio Lourenço, Claude Marché. You-Know-Why: an Early-Stage Prototype of a Key Server Developed using Why3. VerifyThis 2020 - Long-term Challenge, Apr 2020, Dublin, Ireland. pp.4--7. ⟨hal-03002187⟩

Share

Metrics

Record views

15

Files downloads

54

Données de recherche