Ultimate Kojak - (Competition Contribution).
Evren Ermis, Alexander Nutz, Daniel Dietsch, Jochen Hoenicke, Andreas Podelski · Tools and Algorithms for Construction and Analysis of Systems · 2014
Ultimate Kojak is a symbolic software model checker for C programs. It is based on CEGAR and Craig interpolation. The basic algorithm, described in an earlier work [1], was extended to be able to deal with recursive programs using nested word automata and nested (tree) interpolants. 1 Verification Approach Ultimate Kojak computes inductive invariants from interpolants to prove the correctness of a program. A program is represented by a program graph. In a program graph, a vertex is a pair consisting of a program location and an invariant describing the abstract program state. An edge is labelled with a transition formula that corresponds to a block of program statements. A program assertion is represented by a transition to an error state where the transition is labelled with the negated assertion. The goal is to show the unreachability of all error states. The program graph is refined by the algorithm presented in a paper by Ermis et al. [1]. This algorithm computes a sequence of interpolants for an infeasible error path and adds them to the invariant annotated at the corresponding vertices. Since the interpolants are only invariants for the particular error path, we also have to add new vertices for the case where the interpolants do not hold. This is achieved by splitting every vertex on the error path into two new vertices where each receives a new invariant: the old invariant conjoined with the interpolant for the first, and the old invariant conjoined with the negated interpolant for the second. Afterwards, the algorithm removes all infeasible edges, thereby refining the abstraction. The newest version of Ultimate Kojak implements this algorithm and extends it by handling inter-procedural control flow. We use nested word automata to represent programs containing procedures [2]. These automata have call and return transitions and support procedure summaries to prove the correctness of recursive programs. A return transition conceptually has two predecessors: the node representing the call site and the node representing the exit point of the called procedure. Therefore our error paths are in in fact trees. To obtain Corresponding author. E. Abraham and K. Havelund (Eds.): TACAS 2014, LNCS 8413, pp. 421–423, 2014. c © Springer-Verlag Berlin Heidelberg 2014