Zaynah Dargaye, PhD, is a research engineer at CEA List since 2009 and expert in formal languages and verification. She received her PhD from Denis Diderot University (Paris Sorbonne) in 2009 on certified compilation of functional languages. She has been involved in two major projects on formal verification: Frama-C were she contributed to the WP plugin related to deductive analysis of C software in highly-critical domain and CompCert (certified compiler for C) for which she has been awarded the Research Prize of Information Science jointly with her colleagues S. Blazy, X. Leroy and J. B. Tristan.
More recently, she investigated policy languages and trust management to formalize specifications and verification of accountability, liability and privacy in distributed systems. For this purpose, she developed a Cyberlogic theorem prover in Coq thanks to two national projects: SystemX MIC and FUI GeoTransMD.
In 2018, she joined LICIA laboratory to contribute to the design of trust management frameworks to address secure-by-design, and more generally, trust-by-design support framework. Her works have been applied to smart contracts design, verification and enactment on blockchains. This work has resulted in an implementation of audit functionalities for a Start Up Company named Connecting Food in the domain of Food supply Chain. From the specification of the contract, smart-monitors for real-time audit and alerting have been generated that can be formally proved to be compliant with requirements, policies and regulations.