--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on December 2012 ---
Hello, On 12/19/2012 12:07 PM, David MENTRE wrote: > Hello, > > 2012/12/18 Alexey Khoroshilov <khoroshilov at ispras.ru>: >> We use old chain: >> - Nitrogen + Jessie + Why 2 + PVS 5 > [...] >> Linux Verification Center, ISPRAS > Out of curiosity, what are you using Frama-C for? In Linux Verification Center we work on different projects related to static and run-time verification of Linux kernel and userspace. As for the tool chain mentioned (actually, it is Nitrogen + Jessie + Why 2 + alt-ergo/cvc3 + PVS 5), the main purpose is educational. We teach students of Moscow State University (Computer Sciences Department) to Floyd-Hoare analytical verification techniques and we use this tool chain in classes with simple C code. In addition we have a dozen students every year who do their 2-months practice in analytical verification using this tool chain as well. In this case we take more sophisticated code for analysis. It includes functions from Linux kernel and libraries. Most part of kernel space code is not well suit for frama-c/Jessie. Nevertheless, there was a bug in Linux kernel detected: http://git.kernel.org/?p=linux/kernel/git/torvalds/linux.git;a=commitdiff;h=834b40380e93e36f1c9b48ec1d280cebe3d7bd8c -- Best, Alexey Khoroshilov Linux Verification Center, ISPRAS web: http://linuxtesting.org