Verifying Recursive Program via Source-to-Source Program Transformation
Date Issued
2015
Date
2015
Author(s)
Hsieh, Chiao
Abstract
Recursion can complicate program analysis significantly. Some program analyzers simply ignore recursion or even refuse to check recursive programs. In this paper, we propose an algorithm that uses a recursion-free program analyzer as a black box to check recursive programs. With extended program constructs for assumptions, assertions, and non-deterministic values, our algorithm computes function summaries from inductive invariants computed by the underlying program analyzer. Such function summaries enable our algorithm to check recursive programs. We implement a prototype named CPArec using the recursion-free program analyzer CPAchecker. Under the comparison with other program analyzers on the benchmarks in the 2014 and 2015 Competitions on Software Verification, our tool shows competitive efficiency and effectiveness on verifying programs with recursion. Key words: CPArec, Software Verification, Program Analysis, Static Analysis, Recursion, Program Transformation
Subjects
CPArec
Software Verification
Program Analysis
Static Analysis
Recursion
Program Transformation
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-104-R02943142-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):3c6966ad483f387f7749dda4bcf704a6