GUPEA >
IT Faculty / ITfakulteten >
Department of Computer Science and Engineering / Institutionen för data och informationsteknik >
Doctoral Theses / Doktorsavhandlingar Institutionen för data och informationsteknik >
Calculi for Program Incorrectness and Arithmetic
Please use this identifier to cite or link to this item:
http://hdl.handle.net/2077/18717

Title:  Calculi for Program Incorrectness and Arithmetic 
Authors:  Rümmer, Philipp 
Email:  philipp@cs.chalmers.se 
Issue Date:  18Nov2008 
University:  University of Gothenburg. ITFaculty & Chalmers University of Technology 
Institution:  Department of Computer Science and Engineering 
Date of Defence:  20081217 
Disputation:  Onsdagen den 17 december 2008, kl. 10.15, sal EA, vån 4, Hörsalsvägen 11, Chalmers tekniska högskola 
Degree:  Doctor of Philosophy 
Publication type:  Doctoral thesis 
Series/Report no.:  Technical Report D 50 
Abstract:  This thesis is about the development and usage of deductive methods in two
main areas: (i) the deductive disverification 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 firstorder 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 firstorder logic. The
procedure has similarities both with SMTsolvers and with the methods used in
automated firstorder theorem provers. It is complete for theorems of firstorder
logic, decides Presburger arithmetic, and is complete for a substantial fragment
of the combination of both.... more 
ISBN:  9789162872427 
URI:  http://hdl.handle.net/2077/18717 
Appears in Collections:  Doctoral Theses / Doktorsavhandlingar Institutionen för data och informationsteknik Doctoral Theses from University of Gothenburg / Doktorsavhandlingar från Göteborgs universitet
