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]

Latest News

FORSYTE’s 2018 paper awards

FORSYTE has had a quite successful year: Adrian Rebola Pardo and his co-authors received the IJCAR best paper award for their paper Extended Resolution Simulates DRAT, Mitra Tabaei Befrouei and her co-authors received an OOPSLA 2018 Distinguished Paper award for their paper Randomized Testing of Distributed Systems with Probabilistic Guarantees, and Thomas Pani received the […]

Continue reading

OOPSLA Distinguished Paper Award

Mitra Tabaei Befrouei and her co-authors from MPI-SWS Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic, received an OOPSLA’18 Distinguished Paper Award for their contribution “Randomized Testing of Distributed Systems with Probabilistic Guarantees” (Open Access article). Congratulations!

Continue reading

Zvonimir Rakamiric visiting FORSYTE

Prof. Zvonimir Rakamiric from the School of Computing at the University of Utah is spending his sabbatical with the FORSYTE group at TU Wien. He is generously sponsored by the Wolfgang Pauli Institute and a Pauli Fellow.

Continue reading

Helmut Veith Stipend Award Ceremony

The Vice Rector for Academic Affairs of TU Wien, Kurt Matyas, will award the scholarship recipient of the Helmut Veith Stipend at the award ceremony on Friday, April 06, 2018 in the Kontaktraum, starting at 17:05.

Continue reading

Full news archive