Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018) — различия между версиями

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

(Batch edit: replace PCRE (\n\n)+(\n) with \2)
 
(не показано 5 промежуточных версий этого же участника)
{{SlidesSection}}
[[File:Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf|left|page=-|300px]]

{{----}}
[[File:{{#setmainimage:Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018)!.jpg}}|center|640px]]
{{LinksSection}}
<!-- * [ Talks page on site] -->
<!-- <blockquote>[©]</blockquote> -->

{{vklink|1333}}                                          
<references/>





<!-- topub -->

[[Категория:ISPRASOPEN-2018]]
[[Категория:Верификация]]
[[Категория:Linux]]
[[Категория:Статический анализ кода]]
{{stats|disqus_comments=0|refresh_time=2020-01-28T13:17:472021-08-31T17:22:08.622525552739|vimeo_plays=45|youtube_comments=0|youtube_plays=6}}7}}

Текущая версия на 12:21, 4 сентября 2021

Докладчик
Илья Захаров.jpg
Илья Захаров

There is still a gap between rapid development of new verification techniques and their practical application. One of major obstacles to performing sound formal verification of large GNU~C programs is the necessity to prepare environment models.

Researchers usually propose laborious ad-hoc solutions for environment modelling. Also, few software verification frameworks automate it but they support a narrow class of software, e.g. device drivers or embedded systems.

This paper proposes a method for automated compositional generation of environment models that supports adapting for project specifics and enables scalable software verification of various software. We evaluated the proposed method on device drivers and subsystems of the Linux kernel as well as on BusyBox applets.

Видео

on youtube

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

Презентация

Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018).pdf
Композиционное моделирование окружения для верификации программ на GNU C (Илья Захаров, ISPRASOPEN-2018)!.jpg

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

Plays:12   Comments:0