This page in English  Fachgruppe Informatik RWTH

Lehr- und Forschungsgebiet Informatik 2

"Programmiersprachen und Verifikation"

LuFG Informatik 2



Mitarbeiter


Leitung: Wissenschaftliche Mitarbeiter:

NameRaumTelefonE-Mail
Cornelius Aschermann, MScRaum 420980-21241cornelius@informatik.rwth-aachen.de
Dipl.-Inform. Fabian EmmesRaum 420880-21211emmes@informatik.rwth-aachen.de
Florian Frohn, MScRaum 420880-21214florian.frohn@informatik.rwth-aachen.de
Dipl.-Inform. Martin PlückerRaum 420880-21211pluecker@informatik.rwth-aachen.de
Dipl.-Inform. Thomas StröderRaum 420980-21241stroeder@informatik.rwth-aachen.de


Ehemalige Mitarbeiter:



Aktuelle Lehrveranstaltungen

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: WS 2001/2002: SS 2001: WS 2000/2001:

Vertiefungsgebiet "Programmiersprachen und Verifikation"

Das Vertiefungsgebiet "Programmiersprachen und Verifikation" befasst sich mit der Theorie und Implementierung von Programmiersprachen und mit Verfahren, um die Korrektheit von Software in solchen Sprachen zu überprüfen. Hierzu werden die folgenden Vorlesungen angeboten:

Forschungsbereiche (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.





Zu den Internet-Seiten des Lehrstuhls Informatik 2

Disclaimer  Fachgruppe Informatik RWTH