bachelor Automatic Correcting of Basic Math Proofs Automatic grading tool for mathematical proofs Splitting Theory of C Programming Language Decomposition theory for C programs An Annotated variant CompCert-Clightgen Extending CompCert for annotated C programs master Formal Verification of Interlocking Systems A formal framework for verifying railway interlocking systems Revisiting Literal Ordering in CAR-Based Model Checking Analyzing and extending CAR-based strategies SuperCAR A parallel bit-level safety model checker phd