Combining Inlining and Contracting for Human Efficient Deductive Verification

Sammanfattning: A function is functionally correct when it behaves according to a specification that describes its input-output behaviour. With deductive verification, it is possible to prove whether a function conforms to its specification or not. The specification is provided in the form of a source code annotation and describes the function’s input-output behaviour using first-order logic. The function and specification are then used to generate logic formulas that, if proven valid, ensure that the function follows the specification.Creating these source annotations, also called contracts, can be difficult, time-consuming and hence, costly. Therefore, reducing the cost by decreasing the human workload would be a significant step toward large scale deductive verification. One way to do so is to use inlining, which eliminates function definitions by replacing all call sites with the function body instead.This thesis explores if and how inlining can be combined with contracting to reduce the human workload by reducing the number of contracts to be written. For this to be possible, a method to estimate the machine effort required to prove an inlined version is needed. In other words, we need to be able to estimate the verification time for a code module. To this end, two Scania code modules and five categories of artificial programs have been measured.By using function metrics and the verification times of the artificial programs, a heuristic was created using regression. This heuristic was then tested on the Scania modules. The results suggest that the artificial modules were not complex enough to accurately predict the Scania modules. However, it was possible to fit the heuristic to the Scania modules so that no estimate of a Scania module was severely off target. In other words, the Scania modules and their inlined versions were similar enough to be roughly estimated with the same function.If this similarity extends to other industry modules, then creating a general heuristic for estimating verification time would be possible