Hi. I'm Adrien Champion. I have a PhD in software safety and worked on critical embedded systems (systems controlling planes, nuclear plants, cars, etc.) during both my PhD and my first postdoc at the University of Iowa with Cesare Tinelli, where I worked on the Kind 2 model checker. I did my second postdoc at the University of Tokyo with Naoki Kobayashi. I worked on higher-order model-checking: I developed the hoice Horn Clause solver which proved quite efficient for problems stemming from higher-order program verification.

I now work at OCamlPro. Currently, most of my work there targets tezos smart contracts, Michelson which is tezos' language for smart contracts, and Liquidity, an OCaml-like (relatively) high-level language which (de)compiles to/from michelson.

I am interested in software safety and strongly-typed high-level languages such as Rust and OCaml. I still occasionally work on (critical) embedded system verification.