This repository contains a small public fragment of the case study we used to evaluate the use of Stainless to construct high-assurance embedded software.
There are two aspects that this case study evaluates:
- generating C code from Stainless (genc)
- verifying such lower-level imperative code
Stainless: https://epfl-lara.github.io/stainless/installation.html
It should run with versions such as 0.9.1.
To run the verification task:
./verify
To generate C-code from Scala using genc functionality of stainless:
./compile
The resulting C files is also committed to the repository and can be found in the gen folder.
To get some flavor of properties proven, consider the function setBlockAsFree in the Scala source code File.scala. Among the interesting properties that we prove is the invariant blockCountInvariant, which is defined in BlockCountInvariant.scala in terms of executable recursive Scala function countStatusFrom.
The corresponding generated code for the entire fragment is in gen/esover.c file with the C function named the same. In the context of the full case study, the generate code, along with certain bridge functions, compiles as a drop-in replacement for parts of the existing C implementation of the file system and exhibits similar performance as the original code (in some cases running faster, in some cases slower due to decisions taken by the C compiler), and with very similar code sizes.
- Stainless Website: https://stainless.epfl.ch
- EPFL-LARA Website: https://lara.epfl.ch/w/
- Ateleris GmbH Website: https://www.ateleris.ch/
This repository is released under the Apache 2.0 license. See the LICENSE file for more information.