Publications

Céline Bellanger, Pierre-Loic Garoche, Matthieu Martel, Célia Picard (2023). Towards proved formal specification and verification of STL operators as synchronous observers. Submitted.

Hamza Bourbouh, Pierre-Loic Garoche, Christophe Garion, Xavier Thirioux (2021). From Lustre to Simulink: reverse compilation for embedded systems applications. ACM Trans. Cyber Phys. Syst..

Cite

Dany Abou Jaoude, Pierre-Loic Garoche, Mazen Farhood (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

Paul Rousse, John Hauser, Pierre-Loic Garoche (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

Anastasia Mavridou, Hamza Bourbouh, Dimitra Giannakopoulou, Thomas Pressburger, Mohammad Hejase, Pierre-Loic Garoche, Johann Schumann (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

Paul Rousse, Pierre-Loic Garoche, Didier Henrion (2020). Parabolic set simulation for reachability analysis of linear time-invariant systems with integral quadratic constraint. European Journal of Control.

PDF Cite DOI

Raphael Cohen, Eric Feron, Pierre-Loic Garoche (2020). Verification and Validation of Convex Optimization Algorithms for Model Predictive Control. Journal of Aerospace Information Systems.

PDF Cite DOI

Anastasia Mavridou, Hamza Bourbouh, Pierre-Loic Garoche, Dimitra Giannakopoulou, Thomas Pressburger, Johann Schumann (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

Sarah H. Q. Li, Assalé Adjé, Pierre-Loic Garoche, Behçet Açıkmeşe (2020). Fixed Points of the Set-Based Bellman Operator.

Cite

Hamza Bourbouh, Guillaume Brat, Pierre-Loic Garoche (2020). CoCoSim: an automated analysis framework for Simulink/Stateflow. Model Based Space Systems and Software Engineering - European Space Agency Workshop (MBSE'20).

Cite

Hamza Bourbouh, Pierre-Loic Garoche, Thomas Loquen, Éric Noulard, Claire Pagetti (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

Sarah H. Q. Li, Assalé, Adjé, Pierre-Loic Garoche, Behçet Açıkmeşe (2020). Bounding Fixed Points of Set-Based Bellman Operator and Nash Equilibria of Stochastic Games.

Cite

Anastasia Mavridou, Hamza Bourbouh, Pierre-Loic Garoche, Mohammad Hejase (2019). Evaluation of the FRET and CoCoSim tools on the Ten Lockheed Martin Cyber-Physical Challenge Problems.

Cite

Victor Magron, Pierre-Loic Garoche, Didier Henrion, Xavier Thirioux (2019). Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems. SIAM J. Control and Optimization.

Cite

Paul Rousse, Pierre-Loic Garoche, Didier Henrion (2019). Parabolic Set Simulation for Reachability Analysis of Linear Time Invariant Systems with Integral Quadratic Constraint. European Control Conference ECC'19, Naples, Italy.

Cite

Farah Benmouhoub, Matthieu Martel, Pierre-Loic Garoche (2019). Improving the Numerical Accuracy of Parallel Programs by Data Mapping. Numerical and Symbolic Abstract Domains, NSAD'19. Porto, Portugal..

Cite

Paul Rousse, Julien Alexandre Dit Sandretto, Alexandre Chapoutot, Pierre-Loic Garoche (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

Pierre-Loic Garoche (2019). Formal Verification of Control System Software. Princeton University Press.

Cite

Cohen Raphael, Eric Feron, Pierre-Loic Garoche (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

Guillaume Davy, Christophe Garion, Pierre-Loic Garoche, Pierre Roux, Xavier Thirioux (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

Guillaume Davy, Eric Feron, Pierre-Loic Garoche, Didier Henrion (2018). Formal verification of an interior point algorithm instanciation. CoRR.

PDF Cite

Guillaume Davy, Eric Feron, Pierre-Loic Garoche, Didier Henrion (2018). Formal verification of an interior point algorithm instanciation.

PDF Cite

Guillaume Davy, Eric Feron, Pierre-Loic Garoche, Didier Henrion (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

Guillaume Davy, Eric Feron, Pierre-Loic Garoche, Didier Henrion (2018). Automatic Generation and Formal Verification of an Interior Point Method Algorithm. Numerical Software Verification, NSV'18, part of FLoC'18. Oxford, UK..

Cite

Eric M. Feron, Raphael P. Cohen, Guillaume Davy, Pierre-Loic Garoche (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

Victor Magron, Pierre-Loic Garoche, Didier Henrion, Xavier Thirioux (2017). Semidefinite Approximations of Reachable Sets for Discrete-time Polynomial Systems.

Cite

Victor Magron, Didier Henrion, Pierre-Loic Garoche, Xavier Thirioux (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

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

Cite

Pierre-Loic Garoche (2017). Rapport final VORACE. RT 2/26614.

Cite

Pierre-Loic Garoche, Xavier Thirioux, Hamza Bourbouh (2017). Rapport final de l'Etude CNES : Vérification formelle de code généré automatiquement - R S16-BS0004-045. RT 2/26308.

Cite

Pierre-Loic Garoche, Xavier Thirioux (2017). Rapport final de l'Etude CNES : Vérification formelle de code généré automatiquement - R S16-BS0004-045 - COMPARAISON SCADE/LUSTRE/SIMULINK. RT 3/26308.

Cite

Pierre-Loic Garoche, Frank Verdine, Alexandre Chapoutot, Sylvain Conchon, Matthieu Martel, Michael Dierkes (2017). Rapport final CAFEIN. RT 3/21071.

Cite

Julien Brunel, Pierre-Loic Garoche, Pierre Roux (2017). PEA Valencia : Etat d'avancement à T0+9. RT 1/26977.

Cite

Julien Brunel, Pierre-Loic Garoche, Pierre Roux (2017). PEA Valencia : Etat d'avancement à T0+3. RT 1/26976.

Cite

Kévin Garanger, Eric Feron, Pierre-Loic Garoche, Julian J. Rimoli, John D. Berrigan, Martha Grover, Kerianne Hobbs (2017). Foundations of Intelligent Additive Manufacturing. CoRR.

PDF Cite

Raphael P. Cohen, Guillaume Davy, Eric M. Feron, Pierre-Loic Garoche (2017). Formal Verification for Embedded Implementation of Convex Optimization Algorithms. IFAC World Congress 2017.

Cite

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

PDF Cite DOI

Hamza Bourbouh, Pierre-Loic Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, Xavier Thirioux (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

Assalé Adjé, Pierre-Loic Garoche, Victor Magron (2017). A Sums-of-Squares Extension of Policy Iterations. Nonlinear Analysis: Hybrid Systems.

PDF Cite DOI

Pierre-Loic Garoche, Didier Henrion, Victor Magron, Xavier Thirioux (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

Pierre-Loic Garoche, Temesghen Kahsai, Xavier Thirioux (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

Timothy Wang, Romain Jobredeaux, Heber Herencia, Pierre-Loic Garoche, Arnaud Dieumegard, Eric Feron, Marc Pantel (2016). From Design to Implementation: An Automated, Credible Autocoding Chain for Control Systems. Advances in Control System Technology for Aerospace Applications.

Cite DOI

Timothy Wang, Pierre-Loic Garoche, Pierre Roux, Romain Jobredeaux, Eric Feron (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

Timothy Wang, Romain Jobredeaux, Marc Pantel, Pierre-Loic Garoche, Eric Feron, Didier Henrion (2016). Credible Autocoding of Convex Optimization Algorithms. Springer Optimization and Engineering.

PDF Cite

Assalé Adjé, Pierre-Loic Garoche, Alexis Werey (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

Assalé Adjé, Pierre-Loic Garoche, Victor Magron (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

Assalé Adjé, Pierre-Loic Garoche, Victor Magron (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

Assalé Adjé, Pierre-Loic Garoche, Victor Magron (2015). Property-based Polynomial Invariant Generation using Sums-of-Squares Optimization. CoRR.

PDF Cite

Pierre-Loic Garoche (2015). Projet CAFEIN - Rapport avancement RA 3/21071.

Cite

Pierre Roux, Pierre-Loic Garoche (2015). Practical Policy Iterations A practical use of policy iterations for static analysis - The quadratic case.. Formal Methods in System Design.

Cite DOI

Project P consortium (2015). Formal specification of Projet P toolset requirements - SP5.T4.

Cite

Timothy Wang, Eric Feron, Romain Jobredeaux, Marc Pantel, Pierre-Loic Garoche, Didier Henrion (2015). Credible autocoding of convex optimization algorithms. 17th British-French-German Conference on Optimization 15-17 June 2015 London, United Kingdom.

Cite

Arnaud Dieumegard, Pierre-Loic Garoche, Temesghen Kahsai, Alice Tailliar, Xavier Thirioux (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

Pierre Roux, Romain Jobredeaux, Pierre-Loic Garoche (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

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

Cite

Assalé Adjé, Pierre-Loic Garoche (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

Assalé Adjé, Pierre-Loic Garoche, Victor Magron (2015). A Sums-of-Squares Extension of Policy Iterations. CoRR.

PDF Cite

Pierre-Loic Garoche, Falk Howar, Temesghen Kahsai, Xavier Thirioux (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

Pierre-Loic Garoche, Arie Gurfinkel, Temesghen Kahsai (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

Virginie Wiels, Alexandre Amiez, Remi Delmas, Pierre-Loic Garoche, Thomas Loquen, Éric Noulard, Claire Pagetti (2014). Rapport d'avancement Forces3 – 1ère année RA 1/21534.

Cite

Assalé Adjé, Pierre-Loic Garoche, Alexis Werey (2014). Quadratic Zonotopes: An extension of Zonotopes to Quadratic Arithmetics. CoRR.

PDF Cite

Pierre-Loic Garoche (2014). Projet CAFEIN - Rapport avancement RA 2/21071.

Cite

CAFEIN project consortium (2014). Preliminary report on clock directed verification and invariant generation WP1 D1.1.

Cite

CAFEIN project consortium (2014). Open-loop analysis of the control program: first proposal WP2 D2.1.

Cite

Timothy Wang, Romain Jobredeaux, Marc Pantel, Pierre-Loic Garoche, Eric Feron, Didier Henrion (2014). Credible Autocoding of Convex Optimization Algorithms. CoRR.

PDF Cite

Pierre Roux, Pierre-Loic Garoche (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

Assalé Adjé, Pierre-Loic Garoche (2014). Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs. CoRR.

PDF Cite

Pierre-Loïc Garoche, Robert Ford (2013). An example conference paper. In ICW.

PDF Cite Project Slides

Pierre-Loic Garoche (2013). Projet CAFEIN - Rapport avancement RA 1/21071.

Cite

Pierre Roux, Pierre-Loic Garoche (2013). Integrating Policy Iterations in Abstract Interpreters.

Cite DOI

Pierre-Loic Garoche, Temesghen Kahsai, Cesare Tinelli (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

Timothy Wang, Romain Jobredeaux, Heber Herencia-Zapana, Pierre-Loic Garoche, Arnaud Dieumegard, Eric Feron, Marc Pantel (2013). From Design to Implementation: an Automated, Credible Autocoding Chain for Control Systems. CoRR.

PDF Cite

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

Cite

Adrien Champion, Remi Delmas, Michael Dierkes, Pierre-Loic Garoche, Romain Jobredeaux, Pierre Roux (2013). Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses. SAE International Journal of Aerospace.

Cite DOI

Adrien Champion, Remi Delmas, Michael Dierkes, Pierre-Loic Garoche, Romain Jobredeaux, Pierre Roux (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

Pierre Roux, Pierre-Loic Garoche (2013). A Polynomial Template Abstract Domain based on Bernstein Polynomials. Numerical Software Verification.

Cite

Pierre-Loic Garoche (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

Virginie Wiels, Remi Delmas, David Doose, Pierre-Loic. Garoche, Jacques Cazin, Guy Durrieu (2012). Formal Verification of Critical Aerospace Software. Aerospace Lab Journal.

PDF Cite

Pierre Roux, Pierre-Loic Garoche, Alexis Werey (2012). TINY: Simple Static Analyzer for Imperative Code and Numerical precision analysis.

PDF Cite

Heber Herencia-Zapana, Romain Jobredeaux, Sam Owre, Pierre-Loic Garoche, Eric Feron, Gilberto Perez, Pablo Ascariz (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

Pierre Roux, Pierre-Loic Garoche (2012). Ocaml library for Semi-Definite Programming (SDP, SOS).

PDF Cite

Pierre-Loic Garoche, Xavier Thiroux, Temesghen Kahsai (2012). LustreC: a modular Lustre compiler.

PDF Cite

Pierre-Loic Garoche, Temesghen Kasai, Cesare Tinelli (2012). Kind-AI, automatic abstract interpreter module for Lustre model-checker Kind.

PDF Cite

Pierre-Loic Garoche, Temesghen Kasai, Cesare Tinelli (2012). Kind,a k-induction based model-checker.

PDF Cite

Pierre-Loic Garoche, Temesghen Kahsai, Cesare Tinelli (2012). Invariant stream generators using automatic abstract transformers based on a decidable logic. CoRR.

PDF Cite

Temesghen Kahsai, Pierre-Loic Garoche, Cesare Tinelli, Mike Whalen (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

Pierre-Loic Garoche (2012). CAVALE - Intégration dans les processus de validation - focus sur les propriétés fonctionnelle. RF 4/14888.

Cite

Pierre Roux, Romain Jobredeaux, Pierre-Loic Garoche, Eric Feron (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

Adrien Champion, Remi Delmas, Pierre-Loic Garoche, Pierre Roux (2011). Towards Cooperation of Formal Methods for the Analysis of Critical Control Systems. SAE International Journal of Aerospace.

Cite DOI

Pierre Roux, Romain Jobredeaux, Pierre-Loic Garoche, Eric Feron (2011). A Generic Ellipsoid Abstract Domain for Linear Time Invariant Systems.

PDF Cite

Pierre-Loic Garoche, Pierre Roux (2011). SMT-AI, abstract interpreter for a temporal extension of SMT-lib.

PDF Cite

Pierre Roux, Pierre-Loic Garoche (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

Pierre-Loic Garoche (2011). CAVALE - Collaboration d'analyses - Choix techniques & Mise en oeuvre. RT 3/14888.

Cite

Pierre Roux, Remi Delmas, Pierre-Loic Garoche (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

Pierre-Loic Garoche (2010). CAVALE - Collaboration d'analyses pour la vérification d'erreurs à l'exécution. RT 2/14888.

Cite

Guy Durrieu, Pierre-Loïc Garoche Frédéric Boniol (2010). 2.1 - Modélisation pour la prise en compte des phénomènes de rayonnements dans les architectures logicielles avioniques. RT 1/16764.

Cite

Jacques Cazin, Xavier Crégut, Pierre-Loic Garoche, Marc Pantel, Virginie Wiels (2009). Qualifiation of tools - D2.5.1 ES-PASS Project. RT 3/13009.

Cite

Pierre-Loïc Garoche, Virginie Wiels Jacques Cazin (2009). New development processes - D2.4.1 ES-PASS Project. RT 2/13009.

Cite

Pierre-Loïc Garoche, Virginie Wiels Jacques Cazin (2009). Impacts of static analysis on current development process - D2.2.1 ES-PASS Project. RT 1/13009.

Cite

Benoit Combemale, Xavier Crégut, Pierre-Loic Garoche, Xavier Thirioux (2009). Essay on Semantics Definition in MDE - An Instrumented Approach for Model Verification. Journal of Software (JSW).

Cite DOI

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

Cite

Jacques Cazin, Pierre-Loic Garoche, Virginie Wiels (2009). ASBAPROD Assurance Basée Produit - Rapport final, RF 4/13733.

Cite

Pierre-Loic Garoche (2008). Static analysis of an actor-based process calculus by abstract interpretation.

Cite

Jacques Cazin, Pierre-Loic Garoche, Virginie Wiels (2008). Assurance basée sur le produit (ASBAPROD), RT 2/13733 .

Cite

Jacques Cazin, Pierre-Loic Garoche, Virginie Wiels (2008). ASBAPROD - Mise en oeuvre systématique de l'approche sur la Phase 1, RT 3/13733.

Cite

Benoit Combemale, Xavier Crégut, Pierre-Loic Garoche, Xavier Thirioux, François Vernadat (2008). A Property-Driven Approach to Formal Verification of Process Models. Enterprise Information Systems.

Cite DOI

Pierre-Loic Garoche, Marc Pantel, Xavier Thirioux (2007). Abstract Interpretation-based Static Safety for Actors. Journal of Software (JSW).

PDF Cite

Benoit Combemale, Pierre-Loic Garoche, Xavier Crégut, Xavier Thirioux, François Vernadat (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

Xavier Thirioux, Benoit Combemale, Xavier Crégut, Pierre-Loic Garoche (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

Benoit Combemale, Xavier Crégut, Pierre-Loic Garoche, Xavier Thirioux (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

Pierre-Loic Garoche, Marc Pantel, Xavier Thirioux (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

Benoit Combemale, Xavier Crégut, Pierre-Loic Garoche, Xavier Thirioux, François Vernadat (2007). A Property-Driven Approach to Formal Verification of Process Models.

Cite DOI

Pierre-Loic Garoche, Marc Pantel, Xavier Thirioux (2006). Concern-based Specification and Analysis using Abstract Interpretation - A Distributed Case.

Cite

Pierre-Loic Garoche, Marc Pantel, Xavier Thirioux (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

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

Cite

Pierre-Loic Garoche, Marc Pantel, Xavier Thirioux (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

Pierre-Loic Garoche, Cyrille Artho (2006). Zen : an Accurate Centralizer for NASA JavaPathFinder.

Cite

Pierre-Loic Garoche, Xavier Thirioux (2006). YASA: Yet Another Static Analyzer.

Cite

Pierre-Loic Garoche, Marc Pantel, Xavier Thirioux (2006). Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation. CoRR.

PDF Cite

Kenji Tei, Christian Sommer, Yoshiaki Fukazawa, Shinichi Honiden, Pierre-Loic Garoche (2006). Adaptive Geographically Bound Mobile Agents. Mobile Ad-hoc and Sensor Networks.

Cite DOI

Cyrille Artho, Pierre-Loic Garoche (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

Pierre-Loic Garoche, Marc Pantel, Xavier Thirioux (2005). Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation.

Cite

Pierre-Loic Garoche (2005). Static Analysis of Actors by Abstract Interpretation.

Cite

Pierre-Loic Garoche (2005). PACSA: a Primitive Actor Calculus Static Analyzer .

PDF Cite