Proceedings of the 2015 Joint International Mechanical, Electronic and Information Technology Conference

Efficient Predicate Analysis of MISRA-­C Programs

Authors
Feng Gao, Li Li, Jie Luo
Corresponding Author
Feng Gao
Available Online December 2015.
DOI
https://doi.org/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)

Volume Title
Proceedings of the 2015 Joint International Mechanical, Electronic and Information Technology Conference
Series
Advances in Computer Science Research
Publication Date
December 2015
ISBN
978-94-6252-129-2
ISSN
2352-538X
DOI
https://doi.org/10.2991/jimet-15.2015.83How to use a DOI?
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/).

Cite this article

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  - https://doi.org/10.2991/jimet-15.2015.83
ID  - Gao2015/12
ER  -