Visible to the public Scalable Verification Framework for C Program

TitleScalable Verification Framework for C Program
Publication TypeConference Paper
Year of Publication2018
AuthorsChen, G., Wang, D., Li, T., Zhang, C., Gu, M., Sun, J.
Conference Name2018 25th Asia-Pacific Software Engineering Conference (APSEC)
Keywordsabstraction refinement, automatic software verification framework, C language, C program verifiers, Complexity theory, compositionality, context aware software verification, extended structural abstraction, lines-of-code, memory consumption, Metrics, model checking, Optimization, program compilers, Program slicing, program verification, program verification problem, property-guided program slicing, pubcrawl, quality assurance, resilience, Resiliency, Safety, safety critical areas, Scalability, scalability issues, scalable verification, scalable verification framework, Software, Software systems, structural abstraction, Through-silicon vias, TSV

Software verification has been well applied in safety critical areas and has shown the ability to provide better quality assurance for modern software. However, as lines of code and complexity of software systems increase, the scalability of verification becomes a challenge. In this paper, we present an automatic software verification framework TSV to address the scalability issues: (i) the extended structural abstraction and property-guided program slicing to solve large-scale program verification problem, saving time and memory without losing accuracy; (ii) automatically select different verification methods according to the program and property context to improve the verification efficiency. For evaluation, we compare TSV's different configurations with existing C program verifiers based on open benchmarks. We found that TSV with auto-selection performs better than with bounded model checking only or with extended structural abstraction only. Compared to existing tools such as CMBC and CPAChecker, it acquires 10%-20% improvement of accuracy and 50%-90% improvement of memory consumption.

Citation Keychen_scalable_2018