The KeY Project
Between 2001 and 2009 I was a member of the KeY project, which is primarily
concerned with the development of a program verification system for
Java. Besides doing research about program verification, I was working
with the following parts of the KeY implementation:
- The framework for proof search strategies (as main developer)
- Reasoning in first-order logic, e.g., metavariables and
e-matching
to handle quantifiers
- Reasoning in
integer arithmetic (as main developer)
- The update formalism