Certified Programming in the heavy presence of pointers: the case for Union-Find
We present a methodology to get correct-by-construction OCaml programs using the Why3 tool.
First, a formal behavioral specification is given in the form of an OCaml module signature extended with type invariants and function contracts, in the spirit of JML.
Second, an implementation is written in the programming language of Why3 and then verified with respect to the specification.
Finally, an OCaml program is obtained by an automated translation.
Several data structures and algorithms have been designed and proved correct within this setting. We will take the opportunuty in this talk to illustrate our methodology with the design and proof of a union-find library.
04/07/2018 15:00
Software Systems
Simão Melo de Sousa is an Associate Professor of Computer Science at the University of Beira Interior where he teaches courses in the area of programming, software engineering, compilation, computational logic, foundations of computing, formal methods and security. He is an expert in reliability and security of computer systems. In particular he is actively developing research on the fundamentals and the design of techniques and tools for the security, formal verification and development of software. He received his PhD degree at INRIA Sophia Antipolis / UNSA (France) on the theme "Tools and techniques for the formal verification of the JavaCard platform”.
