The project aims to improve open source deductive verification tools, so they can be used to prove properties of Linux kernel code. Our efforts are based on 'Frama-C - Jessie plugin - Why3' tool chain.
See build instructions in wiki.
Manager: Alexey Khoroshilov, Evgeny Novikov, Mikhail Mandrykin
Developer: Alexey Khoroshilov, Denis Efremov, Evgeny Novikov, Grigoriy Volkov, Ilja Zakharov, Mikhail Mandrykin
Reporter: Eugene Kornykhin, Nikita Komarov
Customer: Eugene Kornykhin
Technical Writer: Eugene Kornykhin
Project Creator: Alexey Khoroshilov, Denis Efremov, Mikhail Mandrykin