Dynamic Software and Distributed Systems

Welcome Hardened Golo!

The Golo Galaxy has recently be extended by a new project: Hardened Golo.

This sub-project aims at giving some trust into a Golo program by formally proving their correctness. This project has been initiated with the help of two interns: Bertrand CAYEUX and Raphaƫl LAURENT.

Bertrand starded the work and made a first proposition based on a translation of Golo into Java in order to use Krakatoa in front Why to verify a Golo program. He introduced the specification language name “JGolo”. Afterwhat, Raphael continued the work and developped Hardened Golo Version 0.1. He tried to make a direct translation of Golo program into WhyML.

Welcome on board Hardened Golo! :D