Calculi for Program Incorrectness and Arithmetic

Abstract

This thesis is about the development and usage of deductive methods in two main areas: (i) the deductive dis-verification of programs, i.e., how techniques for deductive verification of programs can be used to detect program defects, and (ii) reasoning modulo integer arithmetic, i.e., how to prove the validity (and, in special cases, satisfiability) of first-order formulae that involve integer arithmetic. The areas of program verification and of testing are traditionally considered as complementary: the former searches for a formal proof of program correctness, while the latter searches for witnesses of program incorrectness. Nevertheless, deductive verification methods can discover bugs indirectly: the failure to prove the absence of bugs is interpreted as a sign for the incorrectness of the program. This approach is bound to produce “false positives” and bugs can be reported also for correct programs. To overcome this problem, I investigate how techniques that are normally used for verification can be used to directly prove the incorrectness of programs. This covers both the detection of partial incorrectness (a program produces results that are inconsistent with a declarative specification), and the detection of total incorrectness (a program diverges erroneously). As a prerequisite for both program correctness and incorrectness proofs, I investigate and extend the concept of updates, which is the central component for performing symbolic execution in Java dynamic logic. Updates are systematically developed as an imperative programming language that provides the following constructs: assignments, guards, sequential composition and bounded as well as unbounded parallel composition. Further, I formulate a calculus for integer arithmetic that is tailored to program verification. While restricted to ground problems, the calculus can handle both linear and nonlinear arithmetic (to some degree) and is useful both for automated and interactive reasoning. The calculus for integer arithmetic can naturally be generalised to a standalone procedure for Presburger arithmetic with uninterpreted predicates, which is a logic that subsumes both Presburger arithmetic and first-order logic. The procedure has similarities both with SMT-solvers and with the methods used in automated first-order theorem provers. It is complete for theorems of first-order logic, decides Presburger arithmetic, and is complete for a substantial fragment of the combination of both.