Title :
Interpolation-based model checking for efficient incremental analysis of software
Author :
Fedyukovich, G. ; Hyvarinen, A.E.J. ; Sharygina, Natasha
Author_Institution :
Fac. of Inf., Univ. of Lugano, Lugano, Switzerland
Abstract :
Verification based on model checking has recently obtained an important role in certain software engineering tasks, such as developing operating system device drivers. This extended abstract discusses how model checking can be made more efficient by using the structure from program function calls. We use this idea in two orthogonal ways, both of which fundamentally depend on automatically summarizing the relevant behavior of the function calls based on an earlier verification. The first approach assumes a piece of software needs to be verified with respect to a set of properties, whereas the second approach considers a case where an early version of a software has been verified but needs to be re-verified after an upgrade. These techniques have been implemented in tools FunFrog and eVolCheck for verifying C programs. Both of them have been tested on a range of academic and industrial benchmarks, and provide in many cases an order of magnitude speed-up with respect to the baseline. They seem to scale to programs with thousands of lines of code.
Keywords :
C language; program diagnostics; program verification; software engineering; C program verification; FunFrog; academic benchmark; eVolCheck; industrial benchmark; interpolation-based model checking; program function calls; software engineering task; software incremental analysis; Abstracts; Algorithm design and analysis; Benchmark testing; Computer science; Computers; Model checking; Software;
Conference_Titel :
Design and Diagnostics of Electronic Circuits & Systems (DDECS), 2013 IEEE 16th International Symposium on
Conference_Location :
Karlovy Vary
Print_ISBN :
978-1-4673-6135-4
Electronic_ISBN :
978-1-4673-6134-7
DOI :
10.1109/DDECS.2013.6549778