Why3: Shepherd your herd of provers, Boogie 2011: 1st Int'l Workshop on Intermediate Verification Languages, pp.53-64, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00790310
Cubicle: A parallel SMTbased model checker for parameterized systems -tool paper, Computer Aided Verification -24th International Conference, CAV 2012, pp.718-724, 2012. ,
Tuning the Alt-Ergo SMT Solver for B Proof Obligations, pp.294-297, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01093000
B-specification of relay-based railway interlocking systems based on the propositional logic of the system state evolution, Reliability, Safety and Security of Railway Systems, IJCAR 2019, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-02185230
Double coeur et preuve formelle pour automatismes sil4, Congrès Lambda Mu 20 de Maîtrise des Risques et de Sûreté de Fonctionnement, IJCAR 2016, 2016. ,
Wcet of ocaml bytecode on microcontrollers: An automated method and its formalisation, Proceedings of the 19th International Workshop on Worst-Case Execution Time Analysis, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02340245
Concurrent Programming of Microcontrollers, a Virtual Machine Approach, 8th European Congress on Embedded Real Time Software and Systems, pp.711-720, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01292266
A Generic Virtual Machine Approach for Programming Microcontrollers: the OMicroB Project, 9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01705825
Programming Microcontrollers in Ocaml: the OCaPIC Project, International Symposium on Practical Aspects of Declarative Languages, vol.9131, pp.132-148, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01213289