| dc.description.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. | en |
