This page in English  Fachgruppe Informatik RWTH

Lehr- und Forschungsgebiet Informatik 2

"Programmiersprachen und Verifikation"

LuFG Informatik 2


Leitung: Wissenschaftliche Mitarbeiter:

Dr. Florian Frohn Raum 4209 80-21241
Nils Lommen, MSc Raum 4208 80-21214
Eleanore Meyer, MSc Raum 4208 80-21214
Daniel Cloerkes, MSc Raum 420880-21214
Stefan Dollase, MSc Raum 4209 80-21241
Jan-Christoph Kassing, MSc Raum 4209 80-21241

Ehemalige Mitarbeiter:

Aktuelle Lehrveranstaltungen

SS 2024: WS 2023/2024: SS 2023: WS 2022/2023: SS 2022: WS 2021/2022: SS 2021: WS 2020/2021: SS 2020: WS 2019/2020: SS 2019: WS 2018/2019: WS 2017/2018: SS 2017: WS 2016/2017: SS 2016: WS 2015/2016: SS 2015: 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