Efficient Predicate Analysis of MISRA-­C Programs

DOI

10.2991/jimet-15.2015.83How to use a DOI?

Keywords

MISRA-­C; Predicate Abstraction; Lazy Abstraction; CEGAR; Imperative Predicates

Abstract

Great care needs to be exercised when using C within safety-related systems. MISRA-C defines a suitable subset of C to be used in safety-related software development, which is easier for program analysis. Predicate abstraction refinement is one of the leading approaches to software verification. In this paper, we propose a procedure to analyze MISRA-C program with predicate abstraction efficiently. The efficiency of this process depends on lazy abstraction and imperative predicates set, which are designed for the program abstraction and predicate refinement procedures respectively. Besides, some features have been added to obtain the desired efficiency, such as initial predicates, pointer alias analysis and so on. Experiments show that it can result in a significant reduction of analysis time and improvement of memory usage compared to earlier methods.

Copyright

© 2015, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Feng Gao
AU  - Li Li
AU  - Jie Luo
PY  - 2015/12
DA  - 2015/12
TI  - Efficient Predicate Analysis of MISRA-­C Programs
BT  - Proceedings of the 2015 Joint International Mechanical, Electronic and Information Technology Conference
PB  - Atlantis Press
SP  - 442
EP  - 447
SN  - 2352-538X
UR  - https://doi.org/10.2991/jimet-15.2015.83
DO  - 10.2991/jimet-15.2015.83
ID  - Gao2015/12
ER  -