Research Group Computer Science 2
"Programming Languages and Verification"
|
|
Head:
Research Assistants:
Former Research Assistants:
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:
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.
-
Mechanized Program Verification
In order to guarantee the reliability and correctness of programs, testing is not sufficient. Instead, a
formal verification of programs is required. However, in general such verification proofs can be very
costly and time-consuming. In particular, this holds for large programs used in practice.
Therefore, the goal is to mechanize program verification as much as possible. For that purpose one
has to use proof tools which can verify correctness statements about programs automatically.
Thus, the course focuses on techniques to automate the task of program verification. The essential
proof technique required to handle programs with loops or recursion is induction. Hence, we introduce techniques to mechanize induction proofs for the verification of programs in a simple
functional language. Moreover, we also present methods to prove the termination of programs
automatically.
-
Functional Programming
The course gives an introduction to functional programming using the language Haskell. Moreover,
we discuss models for the semantics and the implementation of functional languages. This also
includes techniques for type checking and type inference as well as methods for the optimization of
functional programs.
-
Term Rewriting Systems
Term rewriting systems are used for computations and mechanized proofs with
equations. All functional programming languages are based on
term rewriting systems, too. Therefore, term rewriting systems are used in many areas
like mechanized program verification, specification of programs and declarative programming.
The following questions will be discussed in the course.
- Is the result of a computation always unique (confluence)?
- Does a computation always stop after a finite number of steps (termination)?
- Does a program fulfill its specification (correctness)?
- How can the completion of an incomplete program be handled automatically?
-
Logic Programming
Apart from a short introduction to the programming language Prolog this
course is concerned with the basics of logic programming, programming
techniques and implementations of logic programming languages.
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).
Homepage of the Chair for Computer Science 2
