The European Space Agency is funding students to participate in the Hi-Lite project through the SOCIS 2012 program. To contribute to this Open-Source project, apply on the page for students on SOCIS website.
The goal of this project is to extend the work already done on a library of containers adapted to formal verification. We aim at:
- Adding formal contracts (preconditions and postconditions) to the existing formal container library.
- Adding a version of the library that can hold indefinite elements, in particular classwide types (which allows in Ada to put objects of a same hierarchy in the same container).
- Possibly adding formal contracts to other critical libraries (input/output, OS operations, etc.)
The student will have access to the formal verification tools developed in Hi-Lite, to perform formal verification on code snippets making use of the libraries.