Linux Deductive Verification
Linux Deductive Verification project aims to improve open source deductive verification tools, so they can be used to prove properties of Linux kernel code. A target for the first round of the project is a custom LSM implementation that is a part of the Astra Linux Special Edition distribution.
We build our efforts on top of the 'Frama-C + Jessie + Why3 IDE' deductive verification toolchain. The toolchain was adapted, so it can be used to prove properties of Linux kernel code. The most of our modifications goes to the Jessie plugin, while the Frama-C front-end and the Why3 platform have got just minor fixes or improvements. Some of our modifications were already applied upstream, while the rest is available in our public repositories.
Subscription to the user's mailing list of Linux Deductive Verification project is available here:
Additional information about our improvements is presented in Astraver Toolset 1.0 Release Notes.