Lehr- und Forschungsgebiet
Informatik 2
"Programmiersprachen und Verifikation"
|
|
Leitung:
Wissenschaftliche Mitarbeiter:
Ehemalige Mitarbeiter:
WS 2024/2025:
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:
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:
- Automatisierte Programmverifikation
Das Ziel der Vorlesung ist die Vermittlung von Techniken zur automatischen
Untersuchung der Korrektheit und Zuverlässigkeit von Programmen. Es
wird gezeigt, wie Induktionsbeweise zur Verifikation von Programmen in
einer einfachen funktionalen Programmiersprache automatisch durchgeführt
werden können und es wird darauf eingegangen, wie auch die Terminierung
von Programmen automatisch gezeigt werden kann.
- Grundlagen der Funktionalen Programmierung
Die Vorlesung behandelt sowohl grundlegende Programmiertechniken in
funktionalen Sprachen als auch die Konzepte, die hinter solchen Sprachen
stehen. Neben einer Einführung in das funktionale Programmieren mit
der Sprache Haskell werden Modelle für die Semantik und die Implementierung
funktionaler Sprachen vorgestellt. Hierbei wird auch auf Verfahren zur
Typüberprüfung und -inferenz eingegangen.
- Termersetzungssysteme
Termersetzungssysteme dienen zum Rechnen und automatischen Beweisen
mit Gleichungen. Außerdem sind Termersetzungssysteme die Basis-Programmiersprache,
die allen funktionalen Programmiersprachen zugrunde liegt. Termersetzungssysteme
werden daher in vielen Bereichen wie der automatisierten Programmverifikation,
der Spezifikation von Programmen und der deklarativen Programmierung eingesetzt.
In der Vorlesung werden daher Verfahren vorgestellt, um folgende Fragestellungen
rechnergestützt zu untersuchen:
- Ist das Resultat einer Berechnung immer eindeutig (Konfluenz)?
- Hält die Berechnung immer nach endlich vielen Schritten an (Terminierung)?
- Erfüllt ein Programm seine Spezifikation (Korrektheit)?
- Wie kann man ein unvollständiges Programm automatisch
vervollständigen?
- Logikprogrammierung
Neben einer kurzen Einführung in die Sprache Prolog behandelt
diese Vorlesung die Grundlagen der logischen Programmierung, logische
Programmiertechniken sowie die Implementierung von Logiksprachen.
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.
- Improving Mechanized Program Verification
The aim of this research project, which was funded by the DFG, is to improve
the existing techniques and systems for mechanized verification of algorithms.
In particular, we examine the problem of automating verification and transformation
of imperative programs. Here, our goal is to apply verification techniques
and systems (e.g., inductive theorem provers) which were designed for functional
programs for correctness proofs of imperative programs as well. To this end,
we developed a procedure to transform imperative programs into functional
ones. In contrast to previous translations, this transformation generates
functional programs that are especially well suited for verification. Another
important topic in this project is the use of such techniques for automated
lemma generation and generalization.
The transformation of imperative programs into functional ones often
generates partial functions. For that reason, we developed techniques in order
to use inductive theorem provers for partial functions, too. In collaboration
with the University of York (UK) we also extended these results to specification
languages like Z.
- Combining Program Verification Techniques and Decision Procedures
Most problems related to the correctness of programs are undecidable.
For that reason, most mechanized program verification systems are interactive.
However, typically the proof of a verification task raises numerous proof
obligations in specific sub-areas which are decidable. For many of those
areas there exist efficient fully automated decision procedures.
Therefore, this project is concerned with the combination of decision
procedures and techniques for mechanized program verification. Together
with the University of New Mexico (USA) we are working on new decision
techniques which can be used for verification tasks which could only be
tackled by interactive provers up to now. In particular, we are developing
a "decidable induction prover" which can decide inductive validity of proof
obligations of a certain form. Thus, in contrast to previous induction
provers, no interaction is required any more, and the prover can only fail
if the proof obligation is indeed not valid. Future work will focus on
extending this prover with further decision procedures in order to increase
its power without compromising its degree of automation.
Moreover, in collaboration with Ericsson Telecom (Stockholm, Sweden)
we are investigating how to combine approaches based on model checking with
inductive theorem proving in order to verify statements about parameterized
distributed networks or about networks of "data-dependent" processes.
- Extension of Techniques for Termination Analysis
In an earlier project funded by the DFG, we have developed automatic techniques
for termination proofs of functional programs and of term rewriting systems
which proved successful on a large collection of practically relevant algorithms.
Our techniques are currently the most powerful ones available for these tasks
and they were implemented in several systems. For more details on our own
system look at the AProVE
website.
Based on these previous results, this project is concerned with
the refinement, extension, and the development of new heuristics for automated
termination analysis. The main topics addressed in this project are:
- Comparison and evaluation of different termination techniques (together
with the University of Tsukuba, Japan)
- Extension of termination techniques to different programming languages
and evaluation strategies (together with the University of Tsukuba,
Japan)
- Termination analysis for algorithms with underlying equations (together
with the University of New Mexico, USA)
- Development of modular approaches for termination which can be used
for component-based software construction (together with the University
of Bielefeld, Germany)
- Application of termination techniques in order to verify security
aspects of distributed telecommunication processes (together with Ericsson
Telecom, Stockholm, Sweden).
Zu den Internet-Seiten des Lehrstuhls
Informatik 2
