Publications & Contributions

The Control Software Verification Workshop was held on June 28th, 2013 in Moffett Field, CA as part of this project. More information can be found on the workshop webpage at

List of publications:

Timothy Wang, Alireza Esna Ashari, Romain Jobredeaux, Éric Feron: Credible Autocoding of Fault Detection Observers. In Proceedings of American Control Conference (ACC), 2014 

Arnaud Venet: The Gauge Domain: Scalable Analysis of Linear Inequality Invariants. In Proceedings of Computer Aided Verification (CAV 2012), Berkeley, California, USA 2012. Lecture Notes in Computer Science, pages 139-154, volume 7358, Springer 2012 (PDF)

Pierre Roux, Romain Jobredeaux, Pierre-Loïc Garoche, and Éric Féron. 2012. A generic ellipsoid abstract domain for linear time invariant systems. In Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control (HSCC '12). (PDF)

Heber Herencia-Zapana, Romain Jobredeaux, Sam Owre, Pierre-Loïc Garoche, Eric Feron, Gilberto Perez, Pablo Ascariz: PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL. In Proceedings of NASA Formal Methods 2012: 147-161 (link) (long version)

Romain Jobredeaux, Timothy Wang, Eric Feron: Autocoding software with proofs I: Annotation translation. In Digital Avionics Systems Conference (DASC), 2011 IEEE/AIAA 30th , pp.7C1-1-7C1-13 (link)