Efficient Predicate Analysis of MISRA--C Programs
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 theprogram abstractionandpredicate refinementprocedures 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.
MISRA--C Predicate Abstraction Lazy Abstraction CEGA Imperative Predicates
Feng Gao Li Li Jie Luo
State Key Lab of Software Development Environment Department of Computer Science and Engineering, Beihang University Beijing 100191, China
国际会议
重庆
英文
442-447
2015-12-18（万方平台首次上网日期，不代表论文的发表时间）