Dongwoo Kim  Yunja Choi

10.5626/JOK.2021.48.2.174

KLEE CBMC multitask program verification

OiL-CEGAR[1] verifies the composition of a formal OS model and an abstracted application program for accurate verification. Due to the use of the abstract program, however false-alarms can be reported and executability checking for identifying false-alarms requires a high cost. Therefore, efficient executability checking is essential to improve verification performance. To find an effective executability checking method, this study introduces and compares two different techniques that perform executability checking. The first one collects the Boolean formula for the entire program and checks the reachability of all the program blocks in the counterexample by using CBMC. While the second one uses KLEE and identifies non-executable blocks in the counterexample through the binary search-based executability checking. The suggested executability checking methods are applied to a window controller program from the automotive domain. Results show that executability checking using KLEE takes only 1/2000 time compared to that of CBMC and reduces 11.78% of OiL-CEGAR verification costs.