|
|
Department of Computer Science |
|
Research Group Computer Science 2"Programming Languages and Verification" |
|
| Name | Room | Phone | |
|---|---|---|---|
| Dr. Florian Frohn | Room 4209 | 80-21241 | florian.frohn@cs.rwth-aachen.de |
| Nils Lommen, MSc | Room 4208 | 80-21214 | lommen@cs.rwth-aachen.de |
| Eleanore Meyer, MSc | Room 4208 | 80-21214 | eleanore.meyer@cs.rwth-aachen.de |
| Daniel Cloerkes, MSc | Room 4208 | 80-21214 | cloerkes@cs.rwth-aachen.de |
| Stefan Dollase, MSc | Room 4209 | 80-21241 | stefan.dollase@cs.rwth-aachen.de |
| Jan-Christoph Kassing, MSc | Room 4209 | 80-21241 | kassing@cs.rwth-aachen.de |
| Jera Hensel, MSc | Room 4209 | 80-21241 | hensel@informatik.rwth-aachen.de |
| David Keller, MSc | Room 4209 | 80-21241 | davidkor@informatik.rwth-aachen.de |
Former Research Assistants:
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.
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.
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.
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.
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:
Homepage of the Chair for Computer Science 2
Disclaimer
Dept. of Computer Science
