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.
Dr. Christoph Sticksel
Senior Team Leader and Principal Software Engineer in
Formal Methods/Program Analysis at
MathWorks
Natick, MA