Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018) — различия между версиями

Материал из 0x1.tv

;{{SpeakerInfo}}: {{Speaker|Григорий Волков}}
<blockquote>
This talk describes the development of an auto-active verification technique in the Frama-C framework. We outline the lemma functions method and present the corresponding ACSL extension, its implementation in Frama-C, and evaluation on a set of string-manipulating functions from the Linux kernel. 

We illustrate the benefits our approach can bring concerning the effort required to prove lemmas, compared to the approach based on interactive provers such as Coq. Current limitations of the method and its implementation are discussed.
</blockquote>

{{VideoSection}}
{{vimeoembed|298788551|800|450}}
{{youtubelink|}}|8Gc_aG9kiEU}}
{{letscomment}}

{{SlidesSection}}
[[File:Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf|left|page=-|300px]]

{{----}}
[[File:{{#setmainimage:Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018)!.jpg}}|center|640px]]
{{LinksSection}}
<!-- * [ Talks page on site] -->
<!-- <blockquote>[©]</blockquote> -->

{{vklink|1321}}                                          
<references/>

Версия 23:08, 21 февраля 2019

Докладчик
Григорий Волков

This talk describes the development of an auto-active verification technique in the Frama-C framework. We outline the lemma functions method and present the corresponding ACSL extension, its implementation in Frama-C, and evaluation on a set of string-manipulating functions from the Linux kernel.

We illustrate the benefits our approach can bring concerning the effort required to prove lemmas, compared to the approach based on interactive provers such as Coq. Current limitations of the method and its implementation are discussed.

Видео

on youtube

Посмотрели доклад? Понравился? Напишите комментарий! Не согласны? Тем более напишите.

Презентация

Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018).pdf
Функции-леммы в среде Frama-C — использование С программ как доказательств (Григорий Волков, ISPRASOPEN-2018)!.jpg

Примечания и ссылки