Verification of I/O behavior of programs in F*
-----------------------------------
          
ABSTRACT
-----------------------------------
The verification of the input/output behavior of programs
proved to be a hard problem. Some of the concepts that
make verification for IO code more complicated than for
algorithms are: we want to specify properties over the
intermediate states, proof of non-termination is desired and
primitives can throw errors.

The programming language F* proposes a semantic framework
based on Dijkstra Monads for specifying and verifying programs
with arbitrary side-effects (like IO). We used this framework
to verify input/output behavior of programs.

In this seminar we will talk about:
1) the programming language F*
2) why Dijkstra Monads supports a wide variety of verification
   styles for effects such as exceptions and input-output
3) what we learned by verifying a small HTTP server that serves
   files, and the problems we encountered

F*: https://www.fstar-lang.org/
Dijkstra Monads in F*: https://arxiv.org/pdf/1903.01237.pdf


The content of the presentation is the result of an internship
at INRIA.
          
SPEAKER(S)
-----------------------------------
ANDRICI Cezar
Universitatea Alexandru Ioan Cuza, Facultatea de Informatica
Masterul de Studii Avansate in Informatica
-----------------------------------