Verified Implementations for Secure and Verifiable Computation. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Guillaume Davy; François Dupressoir; Benjamin Grégoire; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2014)

Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code. - Guillaume Davy; Christophe Garion; Pierre-Loïc Garoche; Pierre Roux 001; Xavier Thirioux (FDL, 2018)

Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm. - Guillaume Davy; Eric Feron; Pierre-Loïc Garoche; Didier Henrion (LPAR, 2018)

Formal verification of an interior point algorithm instanciation. - Guillaume Davy; Eric Feron; Pierre-Loïc Garoche; Didier Henrion (CoRR, 2018)

Génération de codes et d'annotations prouvables d'algorithmes de points intérieurs à destination de systèmes embarqués critiques. (Generation of codes and provable annotations of interior-point algorithms for critical embedded systems). - Guillaume Davy (2018)