Publications

. Fixed Points of the Set-Based Bellman Operator. 2020.

. CoCoSim, a code generation framework for control/command applications An overview of CoCoSim for multi-periodic discrete Simulink models. 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020), 2020.

PDF

. Bridging the Gap Between Requirements and Simulink Model Analysis. Joint Proceedings of REFSQ-2020 Workshops, Doctoral Symposium, Live Studies Track, and Poster Track co-located with the 26th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2020), Pisa, Italy, March 24, 2020, 2020.

PDF

. Bounding Fixed Points of Set-Based Bellman Operator and Nash Equilibria of Stochastic Games. 2020.

. Improving the Numerical Accuracy of Parallel Programs by Data Mapping. Numerical and Symbolic Abstract Domains, NSAD'19. Porto, Portugal., 2019.

. Formal Verification of Control System Software. 2019.

. Credible Autocoding of The Ellipsoid Algorithm Solving Second-Order Cone Programs. 2018 IEEE Conference on Decision and Control (CDC), Fontainebleau, Miami Beach, FL, USA, 2018.

. Ensuring functional correctness of cyber-physical system controllers: from model to code analyses. Forum on Specification and Design Languages, Special session on Logic and Mathematics Behind Design Automation, FDL'18, TU Munich 10.9-12.9.2018., 2018.

. Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm. LPAR-22, 22st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, November 16-21, 2018, 2018.

. Automatic Generation and Formal Verification of an Interior Point Method Algorithm. Numerical Software Verification, NSV'18, part of FLoC'18. Oxford, UK., 2018.

. Validation of Convex Optimization Algorithms and Credible Implementation for Model Predictive Control. AIAA Information Systems-AIAA Infotech @ Aerospace, AIAA SciTech Forum, (AIAA 2017-0562), 2017.

DOI

. Semidefinite Approximations of Reachable Sets for Discrete-Time Polynomial Systems. SIAM Conference on Applied Algebraic Geometry, July 31st – August 4th 2017, Atlanta, GA, USA, 2017.

. Semi-Definite Programs for Discrete-time Piecewise Affine Systems. Journées PGMO (programme Gaspard Monge pour l'optimisation), 2017.

. Rapport final VORACE. RT 2/26614. 2017.

. Foundations of Intelligent Additive Manufacturing. CoRR, 2017.

PDF

. Automatic synthesis of k-inductive piecewise quadratic invariants for switched affine control programs . Computer Languages, Systems & Structures (COMLAN), 2017.

PDF DOI

. Automated analysis of Stateflow models. LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, 2017.

PDF

. Semidefinite Approximations of Reachability Sets for Discrete-time Polynomial Systems. Journées MODE Mathématiques de l'Optimisation et de la DEcision de la SMAI Société de Mathématiques Appliquées et Industrielles, 2016.

. Hierarchical State Machines as Modular Horn Clauses. Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2016, Eindhoven, The Netherlands, 3rd April 2016., 2016.

PDF DOI

. From Design to Implementation: An Automated, Credible Autocoding Chain for Control Systems. Advances in Control System Technology for Aerospace Applications, 2016.

DOI

. Formal Analysis of Robustness at Model and Code Level. 19th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'16, Vienna, Austria, April 12-14, 2016, 2016.

. Quadratic Zonotopes - An Extension of Zonotopes to Quadratic Arithmetics. Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings, 2015.

DOI

. Property-based polynomial invariant generation using sums-of-squares optimization. 17th British-French-German Conference on Optimization 15-17 June 2015 London, United Kingdom, 2015.

. Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization. Static Analysis - 22st International Symposium, SAS 2015, St Malo, France, 2015. Proceedings, 2015.

DOI

. Projet CAFEIN - Rapport avancement RA 3/21071. 2015.

. Credible autocoding of convex optimization algorithms. 17th British-French-German Conference on Optimization 15-17 June 2015 London, United Kingdom, 2015.

. Compilation Of Synchronous Observers As Code Contracts. 30th ACM/SIGAPP Symposium on Applied Computing, SAC 2015, Salamanca, Spain - April 13 - 17, 2015, 2015.

PDF DOI

. Closed Loop Analysis of Control Command Software. 18th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'15, Seattle, Washington, USA, April 14-16, 2015, 2015.

PDF DOI

. Certificate-carrying modular compilation. 10èmes Journées compilation du GDR GPL, 2015.

. Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs. Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, 2015.

DOI

. A Sums-of-Squares Extension of Policy Iterations. CoRR, 2015.

PDF

. Testing-Based Compiler Validation for Synchronous Languages. NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29 - May 1, 2014. Proceedings, 2014.

DOI

. Synthesizing Modular Invariants for Synchronous Code. Proceedings First Workshop on Horn Clauses for Verification and Synthesis, HCVS 2014, Vienna, Austria, 17 July 2014., 2014.

DOI

. Projet CAFEIN - Rapport avancement RA 2/21071. 2014.

. Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison. FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, 2014.

DOI

. Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs. CoRR, 2014.

PDF

. Projet CAFEIN - Rapport avancement RA 1/21071. 2013.

. Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers. NASA Formal Methods - Fifth International Symposium, NFM 2013, Moffett Field, CA USA, May 14-16, 2013. Proceedings, 2013.

DOI

. A Polynomial Template Abstract Domain based on Bernstein Polynomials. Numerical Software Verification, 2013.

. Verification of aircraft controller: from process-based certification to product-based certification. Air Force Safe & Secure Systems & Software Symposium, S5 Conference, Dayton, OH, USA, 2012.

. PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL. NASA Formal Methods - Forth International Symposium, NFM 2012, Norfolk, VA USA, April 3-5, 2012. Proceedings, 2012.

DOI

. Incremental verification with mode variable invariants in state machines. NASA Formal Methods - Forth International Symposium, NFM 2012, Norfolk, VA USA, April 3-5, 2012. Proceedings, 2012.

DOI

. A Generic Ellipsoid Abstract Domain for Linear Time Invariant Systems. Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2012, Beijing, China, April 17-19, 2012, 2012.

PDF DOI

. Towards Cooperation of Formal Methods for the Analysis of Critical Control Systems. SAE International Journal of Aerospace, 2011.

DOI

. Dessine moi un domaine abstrait fini -- une recette à base de Camlp4 et de solveurs SMT. 22èmes Journées Francophones des Langages Applicatifs (JFLA 2011), La Bresse, France, 2011.

PDF

. SMT-AI: an Abstract Interpreter for a Synchronous Extension of SMT-lib. 1st International Workshop on Tools for Automatic Program AnalysiS (TAPAS 2010), SAS'10 satellite event, Perpignan, France, 2010.

DOI

. New development processes - D2.4.1 ES-PASS Project. RT 2/13009. 2009.

. Essay on Semantics Definition in MDE - An Instrumented Approach for Model Verification. Journal of Software (JSW), 2009.

DOI

. CAVALE - Etat de l'art. RT 1/14888. 2009.

. A Property-Driven Approach to Formal Verification of Process Models. Enterprise Information Systems, 2008.

DOI

. Abstract Interpretation-based Static Safety for Actors. Journal of Software (JSW), 2007.

PDF

. Towards a Formal Verification of Process Model's Properties - SimplePDL and TOCL Case Study. International Conference on Enterprise Information Systems (ICEIS), Funchal, Madeira - Portugal, 12/06/07-16/06/07, 2007.

. A Framework to formalise the MDE Foundations. International Workshop on Towers of Models (TOWERS'07), co-located with TOOLS'07, Zurich, 25/06/07, 2007.

. Expérimentation pour la définition d'une sémantique dans l'IDM. Sémantique des (meta)Modèles, Toulouse, France, 29/01/07, 2007.

. Spécification et Vérification par Interprétation Abstraite d'Aspects pour la Distribution. Formalisation des Activités Concurrentes (FAC'07), Toulouse, 15–16 March 2007, 2007.

PDF

. A Property-Driven Approach to Formal Verification of Process Models. 2007.

DOI

. Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation. the 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems, Bologna, Italy (FMOODS'06), 2006.

PDF DOI

. Analyse statique d'un calcul d'acteur par interprétation abstraite. Colloque des doctorants de l'EDIT, 2006.

PDF

. Static Analysis of Actors: From Type Systems to Abstract Interpretation. 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06), ETAPS'06 satellite event, Vienna, Austria, 2006.

PDF

. Adaptive Geographically Bound Mobile Agents. Mobile Ad-hoc and Sensor Networks, 2006.

DOI

. Accurate Centralization for Applying Model Checking on Networked Applications. 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), 18-22 September 2006, Tokyo, Japan, 2006.

PDF