Diese Seite auf deutsch  Department of Computer Science RWTH

Research Group Computer Science 2

"Programming Languages and Verification"

LuFG Informatik 2



Staff


Head: Research Assistants:

NameRoomPhoneE-Mail
Cornelius Aschermann, MScRaum 420980-21241cornelius.aschermann@rwth-aachen.de
Dipl.-Inform. Fabian EmmesRoom 420880-21211emmes@informatik.rwth-aachen.de
Florian Frohn, MScRaum 420880-21214florian.frohn@informatik.rwth-aachen.de
Dipl.-Inform. Martin PlückerRoom 420880-21211pluecker@informatik.rwth-aachen.de
Dipl.-Inform. Thomas StröderRoom 420980-21241stroeder@informatik.rwth-aachen.de


Former Research Assistants:



Current Teaching Activities

WS 2014/2015: SS 2014: SS 2013: WS 2012/2013: SS 2012: WS 2011/2012: SS 2011: WS 2010/2011: SS 2010: WS 2009/2010: WS 2008/2009: SS 2008: WS 2007/2008: SS 2007: WS 2006/2007: SS 2006: WS 2005/2006: SS 2005: SS 2004: WS 2003/2004: SS 2003: WS 2002/2003: SS 2002:

Area of Specialization "Programming Languages and Verification"

The area of specialization "Programming Languages and Verification" is concerned with the theory and implementation of programming languages, and with procedures to analyze the correctness of programs in such languages. The following courses are offered.

Research

Our research group is concerned with several topics from the area of programming languages and verification. In particular, we are interested in the application of formal methods in order to increase the reliability of programs:

To guarantee the correctness of software, testing is not sufficient, but a formal verification is required. Program verification is a highly relevant aspect of software technology and correctness issues are especially important for safety-critical and distributed applications. However, in general mathematical correctness proofs are very expensive and time-consuming. Therefore, program verification should be automated as much as possible.

Thus, a main topic of our research is the development of methods for mechanized analysis and verification of algorithms and systems. For that purpose, we use approaches from areas like term rewriting, automata theory, mathematical logic, computer algebra, and artificial intelligence in order to facilitate the task of correct software development.

A central problem in the design of reliable software is the proof of termination. We have developed the new "dependency pair" method, which extends the applicability of classical techniques for automated termination analysis significantly. For example, our termination proving procedure is used in a project with Ericsson Telecom to guarantee security requirements of distributed telecommunication processes.

Moreover, we work on methods and systems for proving partial correctness of programs. These techniques check if a program meets its specification provided that it terminates. In particular, we are interested in applying such techniques for several types of programming languages and paradigms. For example, we developed a program transformation system which allows the mechanized verification of imperative programs without the use of loop invariants.

Other important topics of our research are concerned with term rewriting, semantics of programming languages, evaluation strategies, modularity aspects of programs, and formal specification languages.





Homepage of the Chair for Computer Science 2

Disclaimer  Dept. of Computer Science RWTH