Programming Languages and Verification

Today we live in a world where software is ubiquitous - from the full-blown workstation application down to the control software in a digital clock. The complexity of this software is continuously growing as even mobile phones approach the power and versatility of desktop computers from 5 years ago. Building functional, stable, and usable software has become one of the main challenges in new product development.

Our group addresses this challenge by supporting the software development process with more powerful analysis tools and programming languages based on strong mathematical principles. The main disciplines to support this approach are logics, formal methods, and automated reasoning and we apply these to program verification and transformations as well as to programming language design and implementation.

One main focus is on the development of automated tools that can verify that a program written in Java, Haskell, or Prolog terminates, i.e., that it does not run forever. Our approach is to translate the given programs into a basic computation mechanism (term rewriting) and continue the analysis there. In this way, our research can in principle be applied to any program written in any language.

We are also interested in code reachability analysis, liveness and safety properties, theorem proving, and improvements for static analysis and language implementations.

The field of software verification requires the combination of many disciplines (program semantics, constraint solving, logics, efficient algorithms, tool integration) and, therefore, research is carried out in close cooperation with research groups in other universities and companies:

- RWTH Aachen University, Aachen, Germany
- University of New Mexico, Albuquerque, USA
- Ben Gurion University, Beer-Sheva, Israel
- Eindhoven University of Technology, Eindhoven The Netherlands
- University of Innsbruck, Innsbruck, Austria
- Katholieke Universiteit Leuven, Leuven, Belgium
- Microsoft Research, Redmond, USA
- Universidad Politecnica de Valencia, Valencia, Spain

Peter Schneider-Kamp

Fabrizio Montesi

Luís Cruz-Filipe

To give you the best possible experience, this site uses cookies Read more about cookies

Accept cookies