Cassis-Verif

Software model checking flight software

Software verification entails the algorithmic analysis of programs to mathematically prove properties of their executions - to prove that given certain assumptions, the code is correct and bug-free. We seek to investigate semi-automation of this process in the context of mission-critical space software. We envision (i) appropriate abstractions and automation tools tailored to this challenging domain, as well as making steps towards (ii) integrating software verification into the development process.

Cassis-Verif is funded by and takes place at the University of Bern. The Space Software Group contributes towards project goals through association with the Software Engineering Group.