Flux publications Open Science ISAE-SUPAERO

Alexandre Dit Sandretto Julien, Chapoutot Alexandre, Garion Christophe, Thirioux Xavier, A Constraint Programming Approach for Polytopic Simulation of Ordinary Differential Equations. 2024, Acta Cybernetica. 26 (4). ISSN 0324-721X

A Constraint Programming Approach for Polytopic Simulation of Ordinary Differential Equations

Brun, Lélio, Garion Christophe, Garoche Pierre-Loic, Thirioux Xavier, Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation. 2023, ACM Transactions on Embedded Computing Systems. 22 (5). 1–24. ISSN 1539-9087

Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation

Pollien, Baptiste, Garion Christophe, Hattenberger Gautier, Roux Pierre, Thirioux Xavier, A Verified UAV Flight Plan Generator : 2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE). 2023, 11th International Conference on Formal Methods in Software Engineering (FormaliSE), 2023-05-15 - 2023-05-14 (2023-05-14, Melbourne)

A Verified UAV Flight Plan Generator : 2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE)

Saqui-Sannes Pierre de, Vingerhoeds Rob A., Garion Christophe, Thirioux Xavier, A Taxonomy of MBSE Approaches by Languages, Tools and Methods. 2022, IEEE Access. 10. 120936-120950. ISSN 2169-3536

A Taxonomy of MBSE Approaches by Languages, Tools and Methods

Bourbouh Hamza, Garoche Pierre-Loic, Garion Christophe, Thirioux Xavier, From Lustre to Simulink : reverse compilation for verifying Embedded Systems Applications. 2021, ACM Transactions on Cyber-Physical Systems. 5 (3). 1-20. ISSN 2378-962X

From Lustre to Simulink: reverse compilation for verifying Embedded Systems Applications

Alexandre Dit Sandretto Julien, Chapoutot Alexandre, Garion Christophe, Thirioux Xavier, Ziat Ghiles, Constraint-based Verification of Formation Control : 2021 60th IEEE Conference on Decision and Control (CDC). 2021, 60th IEEE Conference on Decision and Control, 2021-12-14 - 2021-12-17 (2021-12-17, Austin)

Constraint-based Verification of Formation Control : 2021 60th IEEE Conference on Decision and Control (CDC)

Pollien Baptiste, Garion Christophe, Hattenberger Gautier, Roux Pierre, Thirioux Xavier, Verifying the Mathematical Library of an UAV Autopilot with Frama-C : Formal Methods for Industrial Critical Systems. 2021, Formal Methods for Industrial Critical Systems - FMICS 2021, 2021-08-24 - 2021-08-26 (2021-08-26, Paris)

Verifying the Mathematical Library of an UAV Autopilot with Frama-C : Formal Methods for Industrial Critical Systems

Pollien Baptiste, Thirioux Xavier, Garion Christophe, Gautier Hattenberger, Roux Pierre, Formal Verification for Autopilot - Preliminary state of the art. 2021. (Published)

Formal Verification for Autopilot - Preliminary state of the art

Ziat Ghiles, Mullier Olivier, Sandretto Julien Alexandre dit, Garion Christophe, Chapoutot Alexandre, Thirioux Xavier, Abstract domains for constraint programming with differential equations : Proceedings of the 9th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains. 2020, Proceedings of the 9th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains, 2020-11-17 - 2020-11-17 (2020-11-17)

Abstract domains for constraint programming with differential equations : Proceedings of the 9th ACM SIGPLAN International Workshop on Numerical and S

Thirioux Xavier, Maffart Alexis, Taylor Series Revisited. 2020. (Unpublished)

Taylor Series Revisited

Thirioux Xavier, Maffart Alexis, Taylor Series Revisited : ICTAC 2019 : Theoretical Aspects of Computing. 2019, International Colloquium on Theoretical Aspects of Computing (ICTAC 2019), 2019-11-04 - 2019-10-31 (2019-10-31, Hammamet)

Taylor Series Revisited : ICTAC 2019: Theoretical Aspects of Computing

Damouche Nasrine, Thirioux Xavier, Benmaghnia Hanane, Martel Matthieu, Dépliage de Boucles Versus Précision Numérique. 2019, 18e journées Approches Formelles dans l’Assistance au Développement de Logiciels, 2019-06-14 - 2019-06-12 (2019-06-12, Toulouse)

Dépliage de Boucles Versus Précision Numérique

Davy Guillaume, Garion Christophe, Garoche Pierre-Loic, Roux Pierre, Thirioux Xavier, Preserving Functional Correctness of Cyber-Physical System Controllers : From Model to Code. 2018, Forum on Specification & Design Languages (FDL 2018), 2018-09-10 - 2018-09-12 (2018-09-12, Munich)

Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code

Bourbouh Hamza, Garoche Pierre-Loic, Garion Christophe, Gurfinkel Arie, Kahsai Temesghen, Thirioux Xavier, Automated analysis of Stateflow models : EPiC Series in Computing, vol. 46. 2017, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2017), 2017-05-12 - 2017-05-07 (2017-05-07, Maun)

Automated analysis of Stateflow models : EPiC Series in Computing, vol. 46

Garoche Pierre-Loic, Kahsai Temesghen, Thirioux Xavier, Hierarchical State Machines as Modular Horn Clauses : EPTCS 219 : Electronic Proceedings in Theoretical Computer Science 219. 2016, 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS 2016) - 2016-04-03 (2016-04-03, Eindhoven)

Hierarchical State Machines as Modular Horn Clauses : EPTCS 219 : Electronic Proceedings in Theoretical Computer Science 219

Chevrou Florent, Hurault Aurélie, Mauran Philippe, Ouederni Meriem, Quéinnec Philippe, Thirioux Xavier, La composition de services dans le monde asynchrone Formalisation et vérification en TLA+ : Actes des 14e journees AFADL. 2015, 14e journees Approches Formelles dans l’Assistance au Développement de Logiciels (AFADL 2015), 2015-06-10 - 2015-06-09 (2015-06-09, Bordeaux)

La composition de services dans le monde asynchrone Formalisation et vérification en TLA+ : Actes des 14e journees AFADL

Dieumegard Arnaud, Garoche Pierre-Loic, Kahsai Temesghen, Taillar Alice, Thirioux Xavier, Compilation of synchronous observers as code contracts : Proceedings of the 30th Annual ACM Symposium on Applied Computing. 2015, 30th Annual ACM Symposium on Applied Computing (SAC 2015), 2015-04-17 - 2015-04-13 (2015-04-13, Salamanca)

Compilation of synchronous observers as code contracts : Proceedings of the 30th Annual ACM Symposium on Applied Computing

Garoche Pierre-Loic, Howar Folk, Kahsai Temesghen, Thirioux Xavier, Testing-Based Compiler Validation for Synchronous Languages : NFM 2014 : NASA Formal Methods. 2014, 6th International Symposium on NASA Formal Methods (NFM 2014), 2014-05-01 - 2014-04-29 (2014-04-29, Houston, Texas)

Testing-Based Compiler Validation for Synchronous Languages : NFM 2014: NASA Formal Methods

Garion, Christophe, Hattenberger, Gautier, Pollien, Baptiste, Roux, Pierre, Thirioux, Xavier, Formal Verification for Autopilot - Preliminary state of the art

Formal Verification for Autopilot - Preliminary state of the art

Pollien, Baptiste, Garion, Christophe, Hattenberger, Gautier, Roux, Pierre, Thirioux, Xavier, A Verified UAV Flight Plan Generator

A Verified UAV Flight Plan Generator

Bourbouh, Hamza, Garoche, Pierre-Loïc, Garion, Christophe, Thirioux, Xavier, From Lustre to Simulink : reverse compilation for verifying Embedded Systems Applications

From Lustre to Simulink: reverse compilation for verifying Embedded Systems Applications

Alexandre Dit Sandretto, Julien, Chapoutot, Alexandre, Garion, Christophe, Thirioux, Xavier, Ziat, Ghiles, Constraint-based Verification of Formation Control

Constraint-based Verification of Formation Control

Damouche, Nasrine, Thirioux, Xavier, Benmaghnia, Hanane, Martel, Matthieu, Dépliage de Boucles Versus Précision Numérique

Dépliage de Boucles Versus Précision Numérique

Thirioux, Xavier, Maffart, Alexis, Taylor Series Revisited

Taylor Series Revisited

Marcon, Cécile, Allignol, Cyril, Thirioux, Xavier, Picard, Celia, Implémentation des Bigraphes dans Coq

Implémentation des Bigraphes dans Coq

Davy, Guillaume, Garion, Christophe, Garoche, Pierre-Loïc, Roux, Pierre, Thirioux, Xavier, Preserving Functional Correctness of Cyber-Physical System Controllers : From Model to Code

Preserving Functional Correctness of Cyber-Physical System Controllers: From Model to Code

Pollien, Baptiste, Garion, Christophe, Hattenberger, Gautier, Roux, Pierre, Thirioux, Xavier, Verifying the Mathematical Library of an UAV Autopilot with Frama-C

Verifying the Mathematical Library of an UAV Autopilot with Frama-C

Bourbouh, Hamza, Garoche, Pierre-Loïc, Garion, Christophe, Gurfinkel, Arie, Kahsai, Temesghen, Thirioux, Xavier, Automated analysis of Stateflow models

Automated analysis of Stateflow models

Ziat, Ghiles, Mullier, Olivier, Sandretto, Julien Alexandre Dit, Garion, Christophe, Chapoutot, Alexandre, Thirioux, Xavier, Abstract domains for constraint programming with differential equations

Abstract domains for constraint programming with differential equations

Brun, Lélio, Garion, Christophe, Garoche, Pierre-Loïc, Thirioux, Xavier, Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation

Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation

Wasquel, Valentin, Pollien, Baptiste, Garion, Christophe, Thirioux, Xavier, Improving a Verified Flight Plan Generator : New Properties and Code Modifications

Improving a Verified Flight Plan Generator: New Properties and Code Modifications

Saqui-Sannes, Pierre De, Vingerhoeds, Rob A., Garion, Christophe, Thirioux, Xavier, A Taxonomy of MBSE Approaches by Languages, Tools and Methods

A Taxonomy of MBSE Approaches by Languages, Tools and Methods

Garion, Christophe, Hattenberger, Gautier, Pollien, Baptiste, Roux, Pierre, Thirioux, Xavier, A gentle introduction to C code verification using the Frama-C platform

A gentle introduction to C code verification using the Frama-C platform