# Automatic Bound Computation

The undecidability of the Halting problem is a famous result that goes back to the beginnings of computer science. The result says that there is no general method for automatically proving the termination of programs. Note, that this statement does not contradict the fact that in practice it is very well possible to prove termination for important program classes automatically. For example, it was a huge success when the first automatic tool chain was able to automatically prove the termination of Windows Device Drivers. Because drivers run in kernel mode, non-terminating drivers could cause the whole system to hang. Despite this success, termination is not a satisfying answer to most programmers who not only want to know that their programs terminate but also when! In ongoing research we are developing tools and algorithms for automatically deriving complexity bounds. Consider the following programs:

 ```x = y = n; while (x > 0 && y > 0) if(random()) x--; else y--; ``` ```x = y = n; while (x > 0 && y > 0) if(random()) x--; else { y--; x = n; } ``` ```while (n > 0) t := A[n]; while (n > 0 && t = A[n]) n--; ``` ```i := 0; while (i < n) { j := i + 1; while (j < n) { if (random()) { ConsumeResource(); j--; n--; } j++; } i++; } ```

Our tool Loopus automatically establishes that in the first and third program the complexity of the loop is O(n) and O(n2) in the second program. Moreover our tool establishes that ConsumeResource() is only called O(n) times. If you find the above described research exciting, we can offer you a variety of topics for bachelor / master theses and projects for practical course work and student jobs.

It is beneficial, if you bring the following qualities:

• programming skills
• interest in scientific work
• basic knowledge in logic and set-theory
• willingness to study state-of-the-art publications

[Contact Florian Zuleger]

## Doctoral College “Adaptive Distributed Systems”

Call for applications
Start of program in winter semester 2012
Ultimate closing: March 15th, 2013

## Upcoming Course: Ana Sokolova

Course on Coalgebra in Computer Science

March 8 – June 28, 2012 in seminar room Gödel / von Neumann

## Upcoming Course: Johannes Fürnkranz

Course on Inductive Rule Learning

March 12-27, 2012 in seminar room Gödel

## TU Vienna Honorary Doctorate to Ed Clarke

We are glad to announce that TU Vienna will award an honorary doctorate to Ed Clarke. Edmund M. Clarke is among the leading computer scientists of our times. As a professor at Harvard, and, since 1982, at Carnegie Mellon University, he and his group have not only laid the theoretical and logical foundations of model […]

## Opening of Vienna Center for Logic and Algorithms (VCLA) on Jan 25

The Vienna Center for Logic and Algorithms is an initiative of the Faculty of Informatics and funded by a three-year competitive grant of Vienna University of Technology. Embedded into the primary research area Computational Intelligence and the funding priority Computational Logic of the Faculty, the center is promoting international scientific collaboration in logic and algorithms. […]