Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C and Linux verification?

  • Subject: [Frama-c-discuss] Frama-C and Linux verification?
  • From: khoroshilov at ispras.ru (Alexey Khoroshilov)
  • Date: Wed, 19 Dec 2012 14:13:50 +0400
  • In-reply-to: <CAC3Lx=a4PR6R7ApkUniv8XkYkUxhU9qDqKN5RZDaA5FQWyZGxA@mail.gmail.com>
  • References: <CAC3Lx=a4PR6R7ApkUniv8XkYkUxhU9qDqKN5RZDaA5FQWyZGxA@mail.gmail.com>
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