IST Project -- Hardened Golo : Giving some confidence into your Golo code


Number of students

1 or 2.


Golo is a simple, dynamic, weakly-typed language for the JVM created in 2012 as part of the research activities of the DynaMid group of the Centre of Innovation in Telecommunications and Integration of service aka CITI Laboratory.

This language adds the dynamicity into the objects. It means that objects themselves can evolve during time, by adding new methods, new attributs, ... It's also possible to dynamically modify classes provided by the standard API. By instance by adding new method into String. Its called the augmentation.

HardenedGolo is a project aiming in statically verify some Golo code. The static verification could be only the verification of the language semantic (a division is not made by 0) or the verification of the respect of a specification. We are then currently adding the possibility to describe a specification into a Golo program in a JML-like manner, with the syntax of WhyML. This IST project is in the context of this new feature.


In this project, many aspects could be developped, according to the preferences of the students, among them:


[1] Golo :
[2] Krakatoa :
[3] De Win, B., Vanhaute, B., & De Decker, B. (2002). Security through aspect-oriented programming. In Advances in Network and Distributed Systems Security (pp. 125-138). Springer US.
[4] Guitton, J., Kanig, J., & Moy, Y. (2011). Why hi-lite ada. Rustan, et al.[32], 27-39, Boogie - 1st international workshop on Intermediate Verification Languages.
[5] Goichon, F., Salagnac, G., Parrend, P., & Frénot, S. (2013). Static vulnerability detection in Java service-oriented components. Journal of Computer Virology and Hacking Techniques, 9(1), 15-26.
[6] Laurent, R. (2016). Hardened Golo : Donnez de la confiance en votre code Golo,