Efficient Predicate Analysis of MISRA-C Programs
- 10.2991/jimet-15.2015.83How to use a DOI?
- MISRA-C; Predicate Abstraction; Lazy Abstraction; CEGAR; Imperative Predicates
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.
- © 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 - 10.2991/jimet-15.2015.83 ID - Gao2015/12 ER -