Publications

(2023). Towards proved formal specification and verification of STL operators as synchronous observers. Submitted.

(2021). From Lustre to Simulink: reverse compilation for embedded systems applications. ACM Trans. Cyber Phys. Syst..

Cite

(2021). Computing State Invariants Using Point-Wise Integral Quadratic Constraints and the S-Procedure. 2021 American Control Conference, ACC 2021, New Orleans, LA, USA, May 26-28, 2021.

Cite

(2020). A Continuation Method for Computation of H $ınfty$ Gains of Linear Continuous Time Periodic Systems. 2020 59th IEEE Conference on Decision and Control (CDC), Jeju Island, Republic of Korea.

Cite

(2020). The Ten Lockheed Martin Cyber-Physical Challenges: Formalized, Analyzed, and Explained. Proceedings of the 28th IEEE International Requirements Engineering Conference (RE 2020), Industrial Innovation track, Zurich, Switzerland, Augsut 31, 2020.

Cite

(2020). Verification and Validation of Convex Optimization Algorithms for Model Predictive Control. Journal of Aerospace Information Systems.

PDF Cite DOI

(2020). 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.

PDF Cite

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

Cite

(2020). CoCoSim: an automated analysis framework for Simulink/Stateflow. Model Based Space Systems and Software Engineering - European Space Agency Workshop (MBSE'20).

Cite

(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).

PDF Cite

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

Cite

(2019). Evaluation of the FRET and CoCoSim tools on the Ten Lockheed Martin Cyber-Physical Challenge Problems.

Cite

(2019). Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems. SIAM J. Control and Optimization.

Cite

(2019). Parabolic Set Simulation for Reachability Analysis of Linear Time Invariant Systems with Integral Quadratic Constraint. European Control Conference ECC'19, Naples, Italy.

Cite

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

Cite

(2019). Guaranteed Simulation of Dynamical Systems with Integral Constraints & Application on Delayed Dynamical Systems. Workshop on Model-Based Design of Cyber Physical Systems (CyPhy'19).

Cite

(2019). Formal Verification of Control System Software. Princeton University Press.

Cite

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

Cite

(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..

Cite

(2018). Formal verification of an interior point algorithm instanciation. CoRR.

PDF Cite

(2018). Formal verification of an interior point algorithm instanciation.

PDF Cite

(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.

Cite

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

Cite

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

Cite DOI

(2017). Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems.

Cite

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

Cite

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

Cite

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

Cite

(2017). Rapport final CAFEIN. RT 3/21071.

Cite

(2017). PEA Valencia : Etat d'avancement à T0+9. RT 1/26977.

Cite

(2017). PEA Valencia : Etat d'avancement à T0+3. RT 1/26976.

Cite

(2017). Foundations of Intelligent Additive Manufacturing. CoRR.

PDF Cite

(2017). Formal Verification for Embedded Implementation of Convex Optimization Algorithms. IFAC World Congress 2017.

Cite

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

PDF Cite DOI

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

PDF Cite

(2017). A Sums-of-Squares Extension of Policy Iterations. Nonlinear Analysis: Hybrid Systems.

PDF Cite DOI

(2016). 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.

Cite

(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..

PDF Cite DOI

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

Cite DOI

(2016). 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.

Cite

(2016). Credible Autocoding of Convex Optimization Algorithms. Springer Optimization and Engineering.

PDF Cite

(2015). 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.

Cite DOI

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

Cite

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

Cite DOI

(2015). Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization. CoRR.

PDF Cite

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

Cite

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

PDF Cite DOI

(2015). 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.

PDF Cite DOI

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

Cite

(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.

Cite DOI

(2015). A Sums-of-Squares Extension of Policy Iterations. CoRR.

PDF Cite

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

Cite DOI

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

Cite DOI

(2014). Rapport d'avancement Forces3 – 1ère année RA 1/21534.

Cite

(2014). Quadratic Zonotopes: An extension of Zonotopes to Quadratic Arithmetics. CoRR.

PDF Cite

(2014). Credible Autocoding of Convex Optimization Algorithms. CoRR.

PDF Cite

(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.

Cite DOI

(2013). An example conference paper. In ICW.

PDF Cite Project Slides

(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.

Cite DOI

(2013). From Design to Implementation: an Automated, Credible Autocoding Chain for Control Systems. CoRR.

PDF Cite

(2013). Formal methods in project P - SP5.L2.

Cite

(2013). Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses. SAE International Journal of Aerospace.

Cite DOI

(2013). Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses. Formal Methods for Industrial Critical Systems (FMICS'13).

Cite DOI

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

Cite

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

Cite

(2012). Formal Verification of Critical Aerospace Software. Aerospace Lab Journal.

PDF Cite

(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.

Cite DOI

(2012). LustreC: a modular Lustre compiler.

PDF Cite

(2012). Kind-AI, automatic abstract interpreter module for Lustre model-checker Kind.

PDF Cite

(2012). Kind,a k-induction based model-checker.

PDF Cite

(2012). Invariant stream generators using automatic abstract transformers based on a decidable logic. CoRR.

PDF Cite

(2012). 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.

Cite DOI

(2012). 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.

PDF Cite DOI

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

Cite DOI

(2011). A Generic Ellipsoid Abstract Domain for Linear Time Invariant Systems.

PDF Cite

(2011). 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.

PDF Cite

(2010). 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.

Cite DOI

(2009). Qualifiation of tools - D2.5.1 ES-PASS Project. RT 3/13009.

Cite

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

Cite

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

Cite DOI

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

Cite

(2009). ASBAPROD Assurance Basée Produit - Rapport final, RF 4/13733.

Cite

(2008). Assurance basée sur le produit (ASBAPROD), RT 2/13733 .

Cite

(2008). ASBAPROD - Mise en oeuvre systématique de l'approche sur la Phase 1, RT 3/13733.

Cite

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

Cite DOI

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

PDF Cite

(2007). 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.

Cite

(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.

Cite

(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.

Cite

(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.

PDF Cite

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

Cite DOI

(2006). 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).

Cite DOI

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

Cite

(2006). 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.

Cite

(2006). Zen : an Accurate Centralizer for NASA JavaPathFinder.

Cite

(2006). YASA: Yet Another Static Analyzer.

Cite

(2006). Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation. CoRR.

PDF Cite

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

Cite DOI

(2006). 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.

PDF Cite

(2005). Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation.

Cite