Essay on semantics definition in MDE. An instrumented approach for model verification B Combemale, X Crégut, PL Garoche, X Thirioux Journal of Software 4 (9), 943-958, 2009 | 104 | 2009 |
Formal verification of critical aerospace software V Wiels, R Delmas, D Doose, PL Garoche, J Cazin, G Durrieu AerospaceLab, p. 1-8, 2012 | 54 | 2012 |
A generic ellipsoid abstract domain for linear time invariant systems P Roux, R Jobredeaux, PL Garoche, É Féron Proceedings of the 15th ACM international conference on Hybrid Systems …, 2012 | 52 | 2012 |
Accurate centralization for applying model checking on networked applications C Artho, PL Garoche 21st IEEE/ACM International Conference on Automated Software Engineering …, 2006 | 50 | 2006 |
PVS linear algebra libraries for verification of control software algorithms in C/ACSL H Herencia-Zapana, R Jobredeaux, S Owre, PL Garoche, E Feron, ... NASA Formal Methods Symposium, 147-161, 2012 | 43 | 2012 |
A framework to formalise the MDE foundations X Thirioux, B Combemale, X Crégut, PL Garoche International Workshop on Towers of Models (TOWERS 2007), 14-30, 2007 | 41 | 2007 |
A property-driven approach to formal verification of process models B Combemale, X Crégut, PL Garoche, X Thirioux, F Vernadat International Conference on Enterprise Information Systems, 286-300, 2007 | 28 | 2007 |
From design to implementation: an automated, credible autocoding chain for control systems T Wang, R Jobredeaux, H Herencia, PL Garoche, A Dieumegard, É Féron, ... Advances in Control System Technology for Aerospace Applications, 137-180, 2016 | 25 | 2016 |
Incremental invariant generation using logic-based automatic abstract transformers PL Garoche, T Kahsai, C Tinelli NASA Formal Methods Symposium, 139-154, 2013 | 24 | 2013 |
Semidefinite approximations of reachable sets for discrete-time polynomial systems V Magron, PL Garoche, D Henrion, X Thirioux SIAM Journal on Control and Optimization 57 (4), 2799-2820, 2019 | 23 | 2019 |
Towards a Formal Verification of Process Model's Properties-SimplePDL and TOCL Case Study B Combemale, PL Garoche, X Crégut, X Thirioux, F Vernadat 9th International Conference on Enterprise Information Systems, 80-89, 2007 | 20 | 2007 |
Automatic synthesis of piecewise linear quadratic invariants for programs A Adjé, PL Garoche International Workshop on Verification, Model Checking, and Abstract …, 2015 | 17 | 2015 |
Testing-based compiler validation for synchronous languages PL Garoche, F Howar, T Kahsai, X Thirioux NASA Formal Methods Symposium, 246-251, 2014 | 16 | 2014 |
Integrating policy iterations in abstract interpreters P Roux, PL Garoche Automated Technology for Verification and Analysis, 240-254, 2013 | 16 | 2013 |
Formal analysis of robustness at model and code level TE Wang, PL Garoche, P Roux, R Jobredeaux, E Feron Proceedings of the 19th International Conference on Hybrid Systems …, 2016 | 15 | 2016 |
Closed loop analysis of control command software P Roux, R Jobredeaux, PL Garoche Proceedings of the 18th International Conference on Hybrid Systems …, 2015 | 13 | 2015 |
Synthesizing modular invariants for synchronous code PL Garoche, A Gurfinkel, T Kahsai arXiv preprint arXiv:1412.1152, 2014 | 12 | 2014 |
Credible autocoding of convex optimization algorithms T Wang, R Jobredeaux, M Pantel, PL Garoche, E Feron, D Henrion Optimization and Engineering 17 (4), 781-812, 2016 | 11 | 2016 |
Quadratic zonotopes A Adjé, PL Garoche, A Werey Asian Symposium on Programming Languages and Systems, 127-145, 2015 | 11 | 2015 |
Property-based polynomial invariant generation using sums-of-squares optimization A Adjé, PL Garoche, V Magron International Static Analysis Symposium, 235-251, 2015 | 11 | 2015 |