 |
Research interests: program verification and analysis; high-level programming languages; automata-theoretic, algebraic and logical methods; constraints.
Future programming languages will allow the programmer to express more and more high-level properties in the source code and have the compiler check them. In order to make this happen, we need to go from program analysis to verification using automated abstraction. Abstraction is logical reasoning over data and control.
- Projects: AVACS (DFG SFB), Verisoft (BMB+F), eJustice (EU IP)
- Terminator: Termination proofs for systems code
- Conferences: CADE-2005, CFV'05, SOFTMC 2005, LOPSTR'05, JFPC'05, SEFM'05, SAS'05, POPL 2006, WST'06, MTCoord'06, FMICS'06, JFPC'06, SAS'06, SRV'06, CSTVA 2006, SATCP'06, ASIAN'06, TACAS'07, VMCAI'07, SAS'07, FMICS'07
- Workshop: Constraints and Verification, Isaac Newton Institute, Cambridge UK, 8 - 12 May 2006
- Journal: STTT, Steering Committee: ETAPS, VMCAI
- Tools: ARMC-Live, DMC (other tools are under development - please come by to inquire about FoPra's, Software Praktika etc.)
- Invited Talks: CP 2004, FMCO'04, COSMICAH'05