Static Verification Tools for C Programs and Linux Device Drivers: A Survey

The survey considers methods and techniques used in modern static verification tools for C programs. It describes two main approaches Counter Example Guided Abstraction Refinement (CEGAR) and Bounded Model Checking (BMC) and techniques used to efficiently implement them such as Predicate Abstraction...

Full description

Bibliographic Details

Published in:	Труды Института системного программирования РАН
Main Authors:	M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. V. Khoroshilov
Format:	Article
Language:	English
Published:	Russian Academy of Sciences, Ivannikov Institute for System Programming 2018-10-01
Subjects:	верификация статический анализ драйвер устройства операционная система linux
Online Access:	https://ispranproceedings.elpub.ru/jour/article/view/1015