About Me

My experience is in formal methods and automated reasoning, and in building systems for software and hardware verification, following and advancing the state of the art, in order to scale to industrial-size problems provided by customers from academia and industry.

At MathWorks I am working on the Simulink Design Verifier that can verify that your Simulink model corresponds to stated requirements, and is free from certain errors without generating actual code.

Previously, I was a postdoctoral researcher in formal methods with a focus on model checking for verification of hardware and software and in first-order automated theorem proving.

I have also taught several university-level courses on logic, foundations and programming languages as the sole responsible lecturer.

News and Updates

  • Going to CAV 2016 (June 30, 2016)

    I'm attending the CAV conference and workshops this year. I'll be in Toronto July 16-July 23 if you want to meet up.

  • MathWorks Research Faculty Summit (June 5, 2016)

    I discovered a really nice event organized by MathWorks: the annual research faculty summit. Plenty of interesting research being presented, and encouragingly many people mentioned how important verification is for them.

  • Kind 2 Paper at CAV (May 8, 2016)

    Our tool paper about the Kind 2 model checker has been accepted at CAV. We discuss an improved invariant generation and introduce two new features: contract-based compositional reasoning and certificate generation. These features have been developed mainly by my co-authors who are still on the project, evolving my work on re-implementing Kind 2.

  • MathWorks is hiring (January 28, 2016)

    We are looking for another developer to join the Simulink Design Verifier team, see the job posting. Help us add new capabilities to the model checker for Simulink, which is used by big customers in many industries worldwide.

  • Joined The MathWorks (October 15, 2015)

    I took up the exciting opportunity to continue working on model checking in a bigger industrial context by joining MathWorks as a developer on the Simulink Design Verifier team. I will be working out of Munich, Germany, and I'm looking forward to it.

Short Biography

(E-mail me for a full CV)

Before joining The MathWorks, I was a Postdoctoral Research Scholar at the Department of Computer Science at the University of Iowa. With Cesare Tinelli we were working on techniques for model checking safety properties of software in the dataflow language Lustre using the Kind 2 model checker, funded by an AFRL and a NASA grant.

I was awarded a postdoctoral fellowship in the EPSRC PhD Plus scheme (now the EPSRC doctoral prize) at The University of Manchester, UK mentored by Konstantin Korovin. The goal was to investigate applications of my PhD research, and we worked on model checking for hardware verification with effectively propositional reasoning.

I obtained my PhD in Computer Science from The University of Manchester, UK under supervision of Konstantin Korovin and Renate Schmidt. My thesis is entitled “Efficient Equational Reasoning in the Inst-Gen Framework”. (PDF)

I graduated in Informatik (Computer Science) from the University of Karlsruhe (now the Karlsruhe Insititue of Technology, KIT) with a German “Diplom”, which used to be a 4.5 year course roughly equivalent to a combined BSc and MSc degree, and has now been replaced by those two degrees.

I wrote my final dissertation “Automated Theorem Proving in Interactive Proof Construction” (PDF) at the Australian National University, Canberra and NICTA under supervision of Peter Baumgartner (NICTA) and P. H. Schmitt (Uni Karlsruhe).

Picture of me

Dr. Christoph Sticksel

Sr. Software Engineer in
Formal Methods/Program Analysis at