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]

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. […]

Happy New Year 2012!

The FORSYTE team is wishing our friends, colleagues and students a Happy New Year!

Winter School on Verification

The Austrian Society for Rigorous Systems Engineering (ARiSE) and the Vienna Center for Logic and Algorithms (VCLA) are organizing a joint winter school on verification at Vienna University of Technology from 6-10 February 2012. Apart from ARiSE/VCLA students, the school will be open to outside students. Details are available from the VCLA website.

Joint PUMA/ARiSE Workshop in Traunkirchen

From October 3–7 2011 PUMA and ARiSE held a joint workshop in Traunkirchen. Further information is available from the workshop’s website. Photos by Damien Zufferey (full gallery):

Helmut Veith is a founding member of the Austrian Society for Rigorous Systems Engineering

The Austrian Society for Rigorous Systems Engineering (ARiSE) was founded in 2010 to further the research in formal methods for the design of correct computer systems. It brings together top researchers in formal methods in Austria in order to foster collaboration and a common research platform.