Brussels / 1 & 2 February 2020


Gneiss: A Nice Component Framework in SPARK

Gneiss is an abstraction layer for component based environments that aims to provide a foundation for formally provable components. It enables the creation of platform independent, asynchronous components in SPARK and provides function contracts that allow to prove the correct interaction with the underlying platform.


Photo of Johannes Kliemann Johannes Kliemann