Under construction...

Overview

ALISS is an implementation of the toy language LISS extended with support for logical annotations. These allow the generation of verification conditions regarding the program, providing thus a way to formally verify the correctness of the implemented algorithm.

The system was developed by us, José Pedro Correia and José Pedro Magalhães as a project for the first semester of the last year of our courses (LESI). This was done under the supervision of professors Jorge Sousa Pinto and Maria João Frade.

The source code developed during this project is attached to this page. Please note that this code is still under development.