Jean-Frédéric Etienne

Jean-Frédéric Etienne has a PhD in formal methods programming from the Conservatoire National des Arts et Métiers in Paris. He is a research engineer who, before joining IOHK in 2020, worked for 12 years on hazard analysis and formal verification of safety-critical embedded systems in the railway industry. He has a deep knowledge of formal methods techniques, including static analysis, deductive verification, theorem-proving, and model-checking (SAT/SMT solvers). His research activities focus on: normalization and optimization techniques towards model/code minimization for automated formal verification; encoding of model-checking for counterexample detection (BMC) and invariance satisfaction (eg, k-induction and PDR) using SAT/SMT solvers; and automatic test case generation to compute both code and proof coverage.