I have implemented and contributed to automated reasoning systems in my preferred language *OCaml*. Both efficiency in dealing with large logic formulas and interfacing with other solvers have been recurring themes here.

I am working as a developer 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.

The *Kind 2* model checker takes a Lustre program as input and tries to automatically verify given safety properties with k-induction and a variety of additional techniques. It uses the SMT solvers Yices, Z3 or CVC3 and can run in a parallel mode, supported by incremental invariant generation.

The *iProver-Eq*
system is an automated first-order theorem prover based on
the successful *iProver* system. It implements an instantiation-based calculus modulo equality and delegates ground reasoning to an SMT solver, currently supporting CVC3, CVC4 and Z3.

You can find the following side projects developed in other contexts on my Github page.

- cvc4-ocaml: An OCaml interface to the CVC4 SMT solver, currently only supporting the QF_UF theory.
- ocamlczmq: An OCaml interface to the ZeroMQ library, using the CZMQ library as an abstraction layer
- smtlib-mode: An Emacs mode to edit SMTLIB2 files

Dr. Christoph Sticksel

Principal Software Engineer in

Formal Methods/Program Analysis at

MathWorks

Natick, MA