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.

At MathWorks I am leading the team for Simulink Design Verifier and Simulink Coverage. With Simulink Coverage you can measure the quality of a test suite with respect to the behaviors of a model it exercises. Using Simulink Design Verifier you can automatically generate tests to achieve high coverage, as well as statically verify that your model corresponds to stated requirements, and is free from certain errors without generating actual code. Simulink Coverage and Design Verifier are key tools in the MathWorks's offering for verification and validation in a model-based design workflow.

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

  • MathWorks (me!) is hiring (November 4, 2021)

    The Simulink Design Verifier team at MathWorks is hiring. I’m looking for a person with formal methods knowledge and experience in building tools for static analysis. We are a small team with a mature product employing a mix of technologies, and have exciting problems to solve. MathWorks is a great place to work at, we have successful products and our work has real impact in allowing our customers in science and engineering to build better and safer systems.

    Obligatory: we plan to transition to a hybrid work model of three days in the office in January. We’re still fully remote, but the office is open to anybody who prefers to work there.

    For more information contact me, and see the job posting.

  • Meet me at FMCAD (September 25, 2019)

    I'm attending the FMCAD conference and tutorials this year. I'll be in San Jose October 22-25 if you want to meet up.

  • FMCAD Call for Papers (April 14, 2019)

    There still time to submit to the Formal Methods in Computer-Aided Design (FMCAD) conference in San Jose, CA from Oct 22-25. Abstract submission ends May 17 (extended from May 10), and theoretical as well as and tool papers and case studies are welcome. FMCAD is always particularly happy to receive contributions from industry, but nevertheless there are usually plenty of novel academic presentations.

    Call for Papers

  • MathWorks Summer Internship (Jan 10, 2018)

    We have a software engineering internship opening to work on Simulink Design Verifier. If you know a thing or two about formal methods and have experience in building, integrating and evaluating tools, this is a great opportunity for you to learn about our technologies and their use in an industrial context. Contact me if you are interested.

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

Senior Team Leader and Principal Software Engineer in
Formal Methods/Program Analysis at
Natick, MA