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

  • 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

Principal Software Engineer in
Formal Methods/Program Analysis at
MathWorks
Natick, MA

cstickse@mathworks.com