{"id":18,"date":"2019-06-21T00:52:46","date_gmt":"2019-06-20T22:52:46","guid":{"rendered":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/?page_id=18"},"modified":"2024-01-11T15:41:08","modified_gmt":"2024-01-11T14:41:08","slug":"publications","status":"publish","type":"page","link":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/publications\/","title":{"rendered":"Publications"},"content":{"rendered":"\n

2026<\/H2>[hal-05518907]<\/a> Kostia Chardonnet, Jules Chouquet, Axel Kerinec, <\/br>Approximation theory for distant Bang calculus<\/strong><\/br>11th International Conference on Formal Structures for Computation and Deduction (FSCD)<\/i>, Jul 2026, Lisbonne, Portugal. ⟨10.48550\/arXiv.2601.05199⟩<\/a><\/br><\/br>[hal-05588566]<\/a> Fr\u00e9d\u00e9ric Dabrowski, <\/br>Kairos : de la sp\u00e9cification temporelle de s\u00fbret\u00e9 \u00e0 la preuve locale<\/strong><\/br>2026<\/br><\/br>[hal-05342070]<\/a> Fr\u00e9d\u00e9ric Loulergue, Olivia Proust, <\/br>Deductively Verifying Functional Scalable Parallel Programs with Why3<\/strong><\/br>Software and Systems Modeling<\/i>, 2026, ⟨10.1007\/s10270-025-01340-y⟩<\/a><\/br><\/br>

2025<\/H2>[hal-05148512]<\/a> Fr\u00e9d\u00e9ric Loulergue, <\/br>Approches formelles pour les composants et outils syst\u00e8me<\/strong><\/br>Journ\u00e9es Approches Formelles pour l'Assistance au D\u00e9veloppement de Logiciels (AFADL)<\/i>, Jun 2025, Pau, France<\/br><\/br>[hal-05095685]<\/a> Yani Ziani, T\u00e9o Bernier, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, Daniel Gracia Perez, <\/br>Towards Formal Verification of a TPM Software Stack: Achievements and Opportunities<\/strong><\/br>Formal Aspects of Computing<\/i>, 2025, 37 (4), ⟨10.1145\/3743153⟩<\/a><\/br><\/br>[hal-05125414]<\/a> Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, Julien Signoles, <\/br>Projet V\u00c9DYSEC : V\u00e9rification Dynamique de Propri\u00e9t\u00e9s de S\u00e9curit\u00e9<\/strong><\/br>Journ\u00e9es Approches Formelles dans l\u2019Assistance au D\u00e9veloppement du Logiciel (AFADL)<\/i>, Jun 2025, Pau, France<\/br><\/br>[hal-04983000]<\/a> Fr\u00e9d\u00e9ric Dabrowski, Jordan Ischard, <\/br>Functional Reactive Programming with Effects, a more permissive approach<\/strong><\/br>2025<\/br><\/br>[hal-05135592]<\/a> Jordan Ischard, Fr\u00e9d\u00e9ric Dabrowski, Jules Chouquet, Fr\u00e9d\u00e9ric Loulergue, <\/br>Une s\u00e9mantique m\u00e9canis\u00e9e d'un langage FRP avec effets<\/strong><\/br>Journ\u00e9es Approches Formelles pour l'Assistance au D\u00e9veloppement de Logiciels (AFADL)<\/i>, Jun 2025, Pau (France), France<\/br><\/br>[hal-04859489]<\/a> J\u00e9r\u00e9my Damour, Allan Blanchard, Lo\u00efc Correnson, Fr\u00e9d\u00e9ric Loulergue, <\/br>Formalisation d'une analyse de r\u00e9gion pour Frama-C\/WP<\/strong><\/br>36es Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2025)<\/i>, Jan 2025, Roiff\u00e9, France<\/br><\/br>[hal-05126380]<\/a> T\u00e9rence Clastres, Frederic Dabrowski, <\/br>Deductive Verification of Synchronous Reactive Programs<\/strong><\/br>Journ\u00e9es Approches Formelles pour l'Assistance au D\u00e9veloppement de Logiciels (AFADL)<\/i>, Jun 2025, Pau (Universit\u00e9 de Pau), France<\/br><\/br>[hal-04795983]<\/a> Jordan Ischard, Frederic Dabrowski, Jules Chouquet, Fr\u00e9d\u00e9ric Loulergue, <\/br>A Mechanized Formalization of an FRP Language with Effects<\/strong><\/br>ACM Symposium on Applied Computing (SAC)<\/i>, Mar 2025, Sicily, Italy. ⟨10.1145\/3672608.3707907⟩<\/a><\/br><\/br>[hal-05117243]<\/a> Yohan Boichut, Thomas Genet, <\/br>Checking that Equations on Terms define a Finite Set of Equivalence Classes<\/strong><\/br>2025<\/br><\/br>[hal-05133511]<\/a> Myriam Clouet, Thibaud Antignac, Mathilde Arnaud, Julien Signoles, <\/br>Langage de sp\u00e9cification de contexte pour v\u00e9rifier formellement des propri\u00e9t\u00e9s de consentement sur des mod\u00e8les et du code -R\u00e9sum\u00e9 long<\/strong><\/br>Journ\u00e9es Approches Formelles pour l'Assistance au D\u00e9veloppement de Logiciels (AFADL)<\/i>, Jun 2025, Pau, France<\/br><\/br>[hal-05146660]<\/a> Olivier Carton, Jean-Michel Couvreur, Martin Delacourt, Nicolas Ollinger, <\/br>Linear Recurrence Sequence Automata and\u00a0the\u00a0Addition of\u00a0Abstract Numeration Systems<\/strong><\/br>WORDS 2025<\/i>, Jun 2025, Nancy, France. pp.70-82, ⟨10.1007\/978-3-031-97548-6_7⟩<\/a><\/br><\/br>[hal-05351661]<\/a> Jean-Michel Couvreur, Martin Delacourt, Nicolas Ollinger, Pierre Popoli, Jeffrey Shallit, Manon Stipulanti, <\/br>Effective Computation of Generalized Abelian Complexity for Pisot Type Substitutive Sequences<\/strong><\/br>2025<\/br><\/br>

2024<\/H2>[tel-04983014]<\/a> Frederic Dabrowski, <\/br>Formal Methods for Synchronization in Parallel and Concurrent Programming Languages<\/strong><\/br>Computer Science [cs]. Universit\u00e9 d'Orl\u00e9ans, 2024<\/br><\/br>[hal-04354615]<\/a> T\u00e9o Bernier, Yani Ziani, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, <\/br>Combining Deductive Verification with Shape Analysis<\/strong><\/br>27th International Conference on Fundamental Approaches to Software Engineering (FASE)<\/i>, 2024, Luxembourg, Luxembourg. pp.280-289, ⟨10.1007\/978-3-031-57259-3_14⟩<\/a><\/br><\/br>[hal-04605772]<\/a> Yohan Boichut, Adrien Boiret, Vincent Hugot, <\/br>SAT-Based Automated Completion for Reachability Analysis<\/strong><\/br>International Conference on Implementation and Application of Automata<\/i>, Sep 2024, Akita, Japan<\/br><\/br>[hal-04556201]<\/a> Fr\u00e9d\u00e9ric Loulergue, Olivia Proust, <\/br>WhyBSML 0.2<\/strong><\/br>2024, ⟨swh:1:dir:f3889ab751233d7ccb812d6e31cc074452b5e139;origin=https:\/\/hal.archives-ouvertes.fr\/hal-04556201;visit=swh:1:snp:eb9686bbb19def3cd7e40be139923aa5270faed8;anchor=swh:1:rel:0040e1fae30354391bea7e4b4fc245556353fd87;path=\/⟩<\/a><\/br><\/br>[hal-04597523]<\/a> Fr\u00e9d\u00e9ric Loulergue, Julien Tesson, <\/br>Verified Parallel Programming in Coq with Bulk Synchronous Parallel Homomorphisms<\/strong><\/br>17th International Symposium on High-Level Parallel Programming and Applications (HLPP)<\/i>, Jul 2024, Pisa, Italy<\/br><\/br>[hal-04637532]<\/a> Yani Ziani, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, Daniel Gracia P\u00e9rez, <\/br>Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack<\/strong><\/br>18th International Conference on Tests and Proofs (TAP)<\/i>, Sep 2024, Milan (Italie), Italy. ⟨10.1007\/978-3-031-72044-4_5⟩<\/a><\/br><\/br>[hal-04811388]<\/a> Jordan Ischard, <\/br>DeBrLevel - version 1.0.1<\/strong><\/br>2024, ⟨swh:1:dir:24f085f9667a4808f717502bd9d3acce95bc9ee1;origin=https:\/\/doi.org\/10.5281\/zenodo.14245079;visit=swh:1:snp:0ed2436203cb8d38464c915df21308e971a71466;anchor=swh:1:rel:bfa68ace2fee6a94e8c70e674ff0f28894fb53ba;path=\/JordanIschard-DeBrLevel-722dfde\/⟩<\/a><\/br><\/br>[hal-04572043]<\/a> Farid Arfi, H\u00e9l\u00e8ne Coullon, Fr\u00e9d\u00e9ric Loulergue, Jolan Philippe, Simon Robillard, <\/br>An Overview of the Decentralized Reconfiguration Language Concerto-D through its Maude Formalization<\/strong><\/br>ICE 2024: 17th Interaction and Concurrency Experience<\/i>, Jun 2024, Groningen, Netherlands. pp.1-18, ⟨10.4204\/EPTCS.414.2⟩<\/a><\/br><\/br>[hal-04644465]<\/a> Fr\u00e9d\u00e9ric Loulergue, Jordan Ischard, <\/br>SyDPaCC: A Framework for the Development of Verified Scalable Parallel Functional Programs<\/strong><\/br>Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)<\/i>, Oct 2024, Crete Island, Greece. ⟨10.1007\/978-3-031-75380-0_16⟩<\/a><\/br><\/br>[hal-04528312]<\/a> Wolfgang Ahrendt, Fr\u00e9d\u00e9ric Loulergue, Heike Wehrheim, <\/br>Introduction to the Special Collection from the International Conference on Tests and Proofs (TAP) 2020 and 2021<\/strong><\/br>Formal Aspects of Computing<\/i>, 36 (1), pp.1-2, 2024, ⟨10.1145\/3650092⟩<\/a><\/br><\/br>[hal-04654817]<\/a> Farid Arfi, H\u00e9l\u00e8ne Coullon, Fr\u00e9d\u00e9ric Loulergue, Jolan Philippe, Simon Robillard, <\/br>Concerto-D in Maude<\/strong><\/br>2024, ⟨swh:1:dir:32a2fe14ad750c01d73d2bd101ef0c2f2e440f62;origin=https:\/\/hal.archives-ouvertes.fr\/hal-04654817;visit=swh:1:snp:ad21f1e90f6cf2549821eb2142ab6657817241f1;anchor=swh:1:rel:9689c8ed0577d56bfb7885c6ed94e9ce0020eca3;path=\/⟩<\/a><\/br><\/br>[hal-04622131]<\/a> T\u00e9o Bernier, Yani Ziani, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, <\/br>Combiner la v\u00e9rification d\u00e9ductive avec l'analyse de forme<\/strong><\/br>Journ\u00e9es Approches Formelles pour l'Assistance au D\u00e9veloppement de Logiciels (AFADL)<\/i>, Jun 2024, Strasbourg, France<\/br><\/br>[hal-04065774]<\/a> Dara Ly, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, Julien Signoles, <\/br>Sound runtime assertion checking for memory properties via program transformation<\/strong><\/br>Formal Aspects of Computing<\/i>, 2024, 36 (1), pp.4:1-46. ⟨10.1145\/3605951⟩<\/a><\/br><\/br>

2023<\/H2>[hal-04171949]<\/a> Fr\u00e9d\u00e9ric Loulergue, Abdelali Ed-Dbali, <\/br>Verified High Performance Computing: the SyDPaCC Approach<\/strong><\/br>16th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS)<\/i>, Oct 2023, Marrakech, Morocco. ⟨10.1007\/978-3-031-49737-7_2⟩<\/a><\/br><\/br>[hal-04173428]<\/a> Olivia Proust, Fr\u00e9d\u00e9ric Loulergue, <\/br>Verified Scalable Parallel Computing with Why3<\/strong><\/br>21st International Conference on Software Engineering and Formal Methods (SEFM)<\/i>, Nov 2023, Eindhoven, Netherlands. ⟨10.1007\/978-3-031-47115-5_14⟩<\/a><\/br><\/br>[hal-04067909]<\/a> H\u00e9l\u00e8ne Coullon, Ludovic Henrio, Fr\u00e9d\u00e9ric Loulergue, Simon Robillard, <\/br>Component-Based Distributed Software Reconfiguration: a Verification-Oriented Survey<\/strong><\/br>ACM Computing Surveys<\/i>, 2023, 56 (1), pp.1-37. ⟨10.1145\/3595376⟩<\/a><\/br><\/br>[hal-03995588]<\/a> Virginia Niculescu, Fr\u00e9d\u00e9ric Loulergue, <\/br>Guest Editor\u2019s Note: High-Level Parallel Programming 2021<\/strong><\/br>International Journal of Parallel Programming<\/i>, 2023, ⟨10.1007\/s10766-023-00752-x⟩<\/a><\/br><\/br>[hal-04142455]<\/a> Darine Rammal, Wadoud Bousdira, Frederic Dabrowski, <\/br>Synchronous cooperative threading model in MSSL<\/strong><\/br>SAC '23: 38th ACM\/SIGAPP Symposium on Applied Computing<\/i>, 2023, Tallinn, Estonia. pp.1380-1383, ⟨10.1145\/3555776.3577815⟩<\/a><\/br><\/br>[hal-04176159]<\/a> Yani Ziani, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, Daniel Gracia P\u00e9rez, T\u00e9o Bernier, <\/br>Towards Formal Verification of a TPM Software Stack<\/strong><\/br>18th International Conference on integrated Formal Methods (iFM)<\/i>, Nov 2023, Leiden, Netherlands. ⟨10.1007\/978-3-031-47705-8_6⟩<\/a><\/br><\/br>[hal-04142453]<\/a> Fr\u00e9d\u00e9ric Loulergue, Jolan Philippe, <\/br>Towards Verified Scalable Parallel Computing with Coq and Spark<\/strong><\/br>FTfJP 2023 - 25th ACM International Workshop on Formal Techniques for Java-like Programs<\/i>, Jul 2023, Seatle, WA, United States. ⟨10.1145\/3605156.3606450⟩<\/a><\/br><\/br>[hal-04142454]<\/a> Fr\u00e9d\u00e9ric Loulergue, <\/br>Tutorial: Collaborative Analysis and Verification of C Programs with Frama-C<\/strong><\/br>38th IEEE\/ACM International Conference on Automated Software Engineering (ASE)<\/i>, Sep 2023, Kirchberg, Luxembourg<\/br><\/br>

2022<\/H2>[hal-03356610]<\/a> Nirina Andrianarivelo, Pierre R\u00e9ty, <\/br>Modular termination of prefix-constrained term rewrite systems<\/strong><\/br>Information Processing Letters<\/i>, 2022, ⟨10.1016\/j.ipl.2021.106207⟩<\/a><\/br><\/br>[hal-03767722]<\/a> Siva Anantharaman, Sabine Frittella, Benjamin Nguyen, <\/br>Privacy Analysis with a Distributed Transition System and a Data-Wise Metric<\/strong><\/br>Privacy in Statistical Databases (PSD)<\/i>, Sep 2022, PARIS, France. pp.15--30<\/br><\/br>[hal-03623522]<\/a> Siva Anantharaman, Sabine Frittella, Benjamin Nguyen, <\/br>Distributed Transition Systems with Tags for Privacy Analysis<\/strong><\/br>2022<\/br><\/br>

2021<\/H2>[hal-03517397]<\/a> Jules Chouquet, Lionel Vaux, <\/br>An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets<\/strong><\/br>Logical Methods in Computer Science<\/i>, 2021, Volume 17, Issue 4, ⟨10.46298\/lmcs-17(4:22)2021⟩<\/a><\/br><\/br>[hal-03160688]<\/a> Virginia Niculescu, Fr\u00e9d\u00e9ric Loulergue, Adrian Sterca, <\/br>Reflection on the Design of Parallel Programming Frameworks<\/strong><\/br>Evaluation of Novel Approaches to Software Engineering<\/i>, pp.154-181, 2021, ⟨10.1007\/978-3-030-70006-5_7⟩<\/a><\/br><\/br>[hal-03338928]<\/a> Salwa Souaf, Fr\u00e9d\u00e9ric Loulergue, <\/br>Experience report: Teaching code analysis and verification using Frama-C<\/strong><\/br>1st International Workshop on Applicable Formal Methods (appFM)<\/i>, Nov 2021, Beijing, China. ⟨10.4204\/EPTCS.349.5⟩<\/a><\/br><\/br>[hal-03261865]<\/a> Fr\u00e9d\u00e9ric Loulergue, Franz Wotawa, <\/br>Tests and Proofs<\/strong><\/br>Springer, 12740, 2021, Lecture Notes in Computer Science, ⟨10.1007\/978-3-030-79379-1⟩<\/a><\/br><\/br>[hal-03178944]<\/a> Frederic Dabrowski, <\/br>On Single-Valuedness in Textually Aligned SPMD Programs<\/strong><\/br>International Journal of Parallel Programming<\/i>, 2021, International Journal of Parallel Programming, ⟨10.1007\/s10766-021-00710-5⟩<\/a><\/br><\/br>

2020<\/H2>[cea-02879211]<\/a> Dara Ly, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, Julien Signoles, <\/br>Verified Runtime Assertion Checking for Memory Properties<\/strong><\/br>TAP 2020 - 14th International Conference on Tests and Proofs<\/i>, Jun 2020, Bergen, Norway. ⟨10.1007\/978-3-030-50995-8_6⟩<\/a><\/br><\/br>[hal-02317068]<\/a> Virginia Niculescu, Fr\u00e9d\u00e9ric Loulergue, <\/br>Transforming powerlist-based divide-and-conquer programs for an improved execution model<\/strong><\/br>Journal of Supercomputing<\/i>, 2020, 76 (7), pp.22. ⟨10.1007\/s11227-019-02820-x⟩<\/a><\/br><\/br>[hal-03102811]<\/a> Fr\u00e9d\u00e9ric Loulergue, <\/br>Special Issue of the Journal of Logical and Algebraic Methods in Programming on Formal Approaches to Parallel and Distributed Systems 2018<\/strong><\/br>Journal of Logical and Algebraic Methods in Programming<\/i>, 116, Elsevier, pp.100580, 2020, ⟨10.1016\/j.jlamp.2020.100580⟩<\/a><\/br><\/br>[hal-02494416]<\/a> Virginia Niculescu, Fr\u00e9d\u00e9ric Loulergue, Darius Bufnea, Adrian Sterca, <\/br>Pattern-driven Design of a Multiparadigm Parallel Programming Framework<\/strong><\/br>13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE)<\/i>, 2020, Prague, Czech Republic. ⟨10.5220\/0009344100500061⟩<\/a><\/br><\/br>[hal-02870592]<\/a> Frederic Dabrowski, <\/br>Verification of DRMA communications<\/strong><\/br>High-level Parallel Programming and Applications<\/i>, Jul 2020, Porto, Portugal<\/br><\/br>[hal-03628124]<\/a> Frederic Dabrowski, <\/br>The Journal of Supercomputing volume\u00a076,\u00a0page 4976 (2020)<\/strong><\/br>2020<\/br><\/br>

2019<\/H2>[hal-02018651]<\/a> Wadoud Bousdira, Arvid Jakobsson, Frederic Dabrowski, <\/br>Safe Usage of Registers in BSPlib<\/strong><\/br>SAC 2019<\/i>, Apr 2019, Limassol, Cyprus. ⟨10.1145\/3297280.3297421⟩<\/a><\/br><\/br>[hal-01955283]<\/a> Arvid Jakobsson, Frederic Dabrowski, Wadoud Bousdira, <\/br>Safe Usage of Registers in BSPlib (Preprint)<\/strong><\/br>2019<\/br><\/br>[hal-03377146]<\/a> Yohan Boichut, Jean-Michel Couvreur, Xavier Ferry, Mohamadou Tafsir Sakho, <\/br>Modeling Concurrent Behaviors as Words<\/strong><\/br>Verification and Evaluation of Computer and Communication Systems<\/i>, 11847, Springer International Publishing, pp.1-15, 2019, Lecture Notes in Computer Science, ⟨10.1007\/978-3-030-35092-5_1⟩<\/a><\/br><\/br>[hal-03622785]<\/a> Dara Ly, Nikolai Kosmatov, Julien Signoles, Fr\u00e9d\u00e9ric Loulergue, <\/br>Soundness of a Dataflow Analysis for Memory Monitoring<\/strong><\/br>Ada Letters<\/i>, 2019, 38 (2), pp.97-108. ⟨10.1145\/3375408.3375416⟩<\/a><\/br><\/br>[hal-01521746]<\/a> Yohan Boichut, Jacques Chabin, Pierre R\u00e9ty, <\/br>Towards more precise rewriting approximations<\/strong><\/br>Journal of Computer and System Sciences<\/i>, 2019, 104, pp.131-148<\/br><\/br>[hal-02162234]<\/a> Wadoud Bousdira, <\/br>Transforming non textually aligned SPMD programs into textually aligned SPMD programs by using rewriting rules<\/strong><\/br>IEEE\/ACM International Conference on High Performance Computing & Simulation<\/i>, Jul 2019, Dublin, Ireland. pp.982-989<\/br><\/br>[hal-02123709]<\/a> Siva Anantharaman, Peter Hibbs, Paliath Narendran, Micha\u00ebl Rusinowitch, <\/br>Unification modulo Lists with Reverse, Relation with Certain Word Equations<\/strong><\/br>CADE-27 - The 27th International Conference on Automated Deduction<\/i>, Association for Automated Reasoning (AAR), Aug 2019, Natal, Brazil. pp.1--17, ⟨10.1007\/978-3-030-29436-6_1⟩<\/a><\/br><\/br>[tel-03215462]<\/a> Thibaut Tachon, <\/br>Automatic Generation of Bulk-Synchronous Parallel code<\/strong><\/br>Distributed, Parallel, and Cluster Computing [cs.DC]. Universit\u00e9 d'Orl\u00e9ans, 2019. English. ⟨NNT : 2019ORLE3098⟩<\/a><\/br><\/br>[hal-02123648]<\/a> Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michael Rusinowitch, <\/br>Unification modulo Lists with Reverse as Solving Simple Sets of Word Equations<\/strong><\/br>[Research Report] LIFO, Universit\u00e9 d'Orl\u00e9ans; INSA, Centre Val de Loire. 2019<\/br><\/br>[hal-02317127]<\/a> Jolan Philippe, Fr\u00e9d\u00e9ric Loulergue, <\/br>PySke: Algorithmic Skeletons for Python<\/strong><\/br>The 2019 International Conference on High Performance Computing & Simulation (HPCS)<\/i>, Jul 2019, Dublin, Ireland. ⟨10.1109\/HPCS48598.2019.9188151⟩<\/a><\/br><\/br>[hal-02317074]<\/a> Jolan Philippe, Fr\u00e9d\u00e9ric Loulergue, <\/br>Parallel programming with Coq: Map and reduce skeletons on trees<\/strong><\/br>34th ACM\/SIGAPP Symposium on Applied Computing (SAC)<\/i>, Apr 2019, Limassol, Cyprus. pp.1578-1581, ⟨10.1145\/3297280.3299742⟩<\/a><\/br><\/br>[hal-02317055]<\/a> Allan Blanchard, Fr\u00e9d\u00e9ric Loulergue, Nikolai Kosmatov, <\/br>Towards Full Proof Automation in Frama-C Using Auto-active Verification<\/strong><\/br>NFM 2019 - 11th Annual NASA Formal Methods Symposium<\/i>, May 2019, Houston, TX, United States. pp.88-105, ⟨10.1007\/978-3-030-20652-9_6⟩<\/a><\/br><\/br>[hal-02318361]<\/a> Jolan Philippe, Fr\u00e9d\u00e9ric Loulergue, <\/br>Towards automatically optimizing PySke programs (poster)<\/strong><\/br>International Conference on High Performance Computing and Simulation (HPCS)<\/i>, Jul 2019, Dublin, Ireland. ⟨10.1109\/HPCS48598.2019.9188160⟩<\/a><\/br><\/br>[hal-02317118]<\/a> Salwa Souaf, Fr\u00e9d\u00e9ric Loulergue, <\/br>A First Step in the Translation of Alloy to Coq<\/strong><\/br>21st International Conference on Formal Engineering Methods (ICFEM)<\/i>, 2019, Shenzen, China. ⟨10.1007\/978-3-030-32409-4_28⟩<\/a><\/br><\/br>[hal-02317143]<\/a> Allan Blanchard, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, <\/br>La logique contre les fant\u00f4mes: comparaison de deux approches pour la preuve d'un module de listes cha\u00een\u00e9es *<\/strong><\/br>18e journ\u00e9es Approches Formelles dans l'Assistance au D\u00e9veloppement de Logic (AFADL)<\/i>, Jun 2019, Toulouse, France. <\/a><\/br><\/br>[tel-02920363]<\/a> Filip Jakobsson, <\/br>Static Analysis for BSPlib Programs<\/strong><\/br>Distributed, Parallel, and Cluster Computing [cs.DC]. Universit\u00e9 d'Orl\u00e9ans, 2019. English. ⟨NNT : 2019ORLE2005⟩<\/a><\/br><\/br>[hal-02100515]<\/a> Allan Blanchard, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, <\/br>Logic against Ghosts: Comparison of Two Proof Approaches for a List Module<\/strong><\/br>SAC 2019 - The 34th ACM\/SIGAPP Symposium On Applied Computing<\/i>, Apr 2019, Limassol, Cyprus. ⟨10.1145\/3297280.3297495⟩<\/a><\/br><\/br>[hal-02317123]<\/a> Fr\u00e9d\u00e9ric Loulergue, Jolan Philippe, <\/br>Automatic Optimization of Python Skeletal Parallel Programs<\/strong><\/br>19th International Conference on Algorithms and Architectures for Parallel Processing (ICA3PP)<\/i>, Dec 2019, Melbourne, Australia. ⟨10.1007\/978-3-030-38991-8_13⟩<\/a><\/br><\/br>[hal-02317124]<\/a> Fr\u00e9d\u00e9ric Loulergue, Jolan Philippe, <\/br>New List Skeletons for the Python Skeleton Library<\/strong><\/br>PDCAT 2019: 20th International Conference on Parallel and Distributed Computing, Applications and Technologies<\/i>, Dec 2019, Gold Coast, Australia. ⟨10.1109\/PDCAT46702.2019.00077⟩<\/a><\/br><\/br>[hal-02018652]<\/a> Frederic Dabrowski, <\/br>A denotational semantics of textually aligned SPMD Program<\/strong><\/br>Journal of Logical and Algebraic Methods in Programming<\/i>, 2019, ⟨10.1016\/j.jlamp.2019.02.010⟩<\/a><\/br><\/br>

2018<\/H2>[hal-01780553]<\/a> Nirina Andrianarivelo, Pierre Rety, <\/br>Confluence of Prefix-Constrained Rewrite Systems<\/strong><\/br>3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)<\/i>, Jul 2018, Oxford, United Kingdom<\/br><\/br>[hal-01903092]<\/a> Yohan Boichut, Vivien Pelletier, Pierre Rety, <\/br>Approximating any Logic Program by a CS-Program<\/strong><\/br>Rewriting Logic and Its Applications - 12th International Workshop<\/i>, Apr 2018, Thessalonique, Greece. pp.245--260<\/br><\/br>[hal-01818140]<\/a> Arvid Jakobsson, <\/br>Automatic Cost Analysis for Imperative BSP Programs<\/strong><\/br>International Journal of Parallel Programming<\/i>, 2018, ⟨10.1007\/s10766-018-0562-1⟩<\/a><\/br><\/br>[hal-01819035]<\/a> Ga\u00e9tan Hains, Arvid Jakobsson, Youry Khmelevsky, <\/br>Towards formal methods and software engineering for deep learning: Security, safety and productivity for dl systems development<\/strong><\/br>2018 Annual IEEE International Systems Conference (SysCon)<\/i>, Apr 2018, Vancouver, France. ⟨10.1109\/SYSCON.2018.8369576⟩<\/a><\/br><\/br>[cea-02283406]<\/a> Dara Ly, Nikolai Kosmatov, Julien Signoles, Fr\u00e9d\u00e9ric Loulergue, <\/br>Soundness of a Dataflow Analysis for Memory Monitoring<\/strong><\/br>HILT 2018 Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems<\/i>, Nov 2018, Boston, United States. ⟨10.1145\/3375408.3375416⟩<\/a><\/br><\/br>[hal-01643971]<\/a> Frederic Dabrowski, <\/br>Textual Alignment in SPMD Programs<\/strong><\/br>SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing<\/i>, Apr 2018, Pau, France. ⟨10.1145\/3167132.3167254⟩<\/a><\/br><\/br>[hal-01785110]<\/a> Fr\u00e9d\u00e9ric Dabrowski, <\/br>A Denotational Semantics of Textually Aligned SPMD Programs<\/strong><\/br>International Conference on High Performance Computing & Simulation<\/i>, Jul 2018, Orl\u00e9ans, France. ⟨10.1109\/HPCS.2018.00119⟩<\/a><\/br><\/br>[hal-01720401]<\/a> Allan Blanchard, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, <\/br>Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C<\/strong><\/br>Tenth NASA Formal Methods Symposium - NFM 2018<\/i>, Apr 2018, Newport News, United States. ⟨10.1007\/978-3-319-77935-5_3⟩<\/a><\/br><\/br>[hal-02317078]<\/a> Allan Blanchard, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, <\/br>A Lesson on Verification of IoT Software with Frama-C<\/strong><\/br>2018 International Conference on High Performance Computing & Simulation (HPCS)<\/i>, Jul 2018, Orleans, France. pp.21-30, ⟨10.1109\/HPCS.2018.00018⟩<\/a><\/br><\/br>[hal-01811922]<\/a> Fr\u00e9d\u00e9ric Loulergue, Allan Blanchard, Nikolai Kosmatov, <\/br>Ghosts for Lists: from Axiomatic to Executable Specifications<\/strong><\/br>TAP 2018 - 12th International Conference on Tests and Proofs<\/i>, Jun 2018, Toulouse, France. ⟨10.1007\/978-3-319-92994-1_11⟩<\/a><\/br><\/br>[hal-01811932]<\/a> Allan Blanchard, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, <\/br>Des listes et leurs fant\u00f4mes : v\u00e9rification d'un module critique de Contiki avec FRAMA-C<\/strong><\/br>17\u00e8mes Journ\u00e9es AFADL : Approches Formelles Dans L'assistance Au D\u00e9veloppement De Logiciels<\/i>, Jun 2018, Toulouse, France<\/br><\/br>[hal-01777123]<\/a> Allan Blanchard, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, <\/br>MMFilter: A CHR-Based Solver for Generation of Executions under Weak Memory Models<\/strong><\/br>Computer Languages, Systems and Structures<\/i>, 2018, 53, pp.121-142. ⟨10.1016\/j.cl.2018.03.002⟩<\/a><\/br><\/br>

2017<\/H2>[hal-01494832]<\/a> Arvid Jakobsson, Frederic Dabrowski, Wadoud Bousdira, Fr\u00e9d\u00e9ric Loulergue, Gaetan Hains, <\/br>Replicated Synchronization for Imperative BSP Programs<\/strong><\/br>International Conference on Computational Science (ICCS)<\/i>, 2017, Z\u00fcrich, Switzerland. ⟨10.1016\/j.procs.2017.05.123⟩<\/a><\/br><\/br>[hal-02317110]<\/a> Jolan Philippe, Wadoud Bousdira, Fr\u00e9d\u00e9ric Loulergue, <\/br>Formalization of a Big Graph API in Coq<\/strong><\/br>2017 International Conference on High Performance Computing & Simulation (HPCS)<\/i>, Jul 2017, Genoa, France. IEEE, 108, pp.893-894, 2017, ⟨10.1109\/HPCS.2017.140⟩<\/a><\/br><\/br>[hal-01159182]<\/a> Fr\u00e9d\u00e9ric Loulergue, Wadoud Bousdira, Julien Tesson, <\/br>Calculating Parallel Programs in Coq using List Homomorphisms<\/strong><\/br>International Journal of Parallel Programming<\/i>, 2017, 45 (2), pp.300-319. ⟨10.1007\/s10766-016-0415-8⟩<\/a><\/br><\/br>[hal-01495453]<\/a> Thibaut Tachon, Chong Li, Ga\u00e9tan Hains, Fr\u00e9d\u00e9ric Loulergue, <\/br>Automated generation of BSP automata<\/strong><\/br>Parallel Processing Letters<\/i>, 2017, 17 (1), ⟨10.1142\/S0129626417400023⟩<\/a><\/br><\/br>[hal-01495454]<\/a> Allan Blanchard, Fr\u00e9d\u00e9ric Loulergue, Nikolai Kosmatov, <\/br>From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation<\/strong><\/br>Fifth International Workshop on Verification and Program Transformation (VPT 2017)<\/i>, Apr 2017, Uppsala, Sweden. ⟨10.4204\/EPTCS.253.9⟩<\/a><\/br><\/br>[hal-01445668]<\/a> Nirina Andrianarivelo, Vivien Pelletier, Pierre R\u00e9ty, <\/br>Transforming Prefix-Constrained or Controlled Rewrite Systems<\/strong><\/br>8th International Symposium on Symbolic Computation in Software Science (SCSS 2017)<\/i>, Apr 2017, Gammarth, Tunisia<\/br><\/br>[hal-02317112]<\/a> Christopher Whitney, Fr\u00e9d\u00e9ric Loulergue, <\/br>Towards a Verified Parallel Implementation of Frequent Itemset Mining<\/strong><\/br>2017 International Conference on High Performance Computing & Simulation (HPCS)<\/i>, Jul 2017, Genoa, Italy. IEEE, pp.889-890, ⟨10.1109\/HPCS.2017.138⟩<\/a><\/br><\/br>[hal-02317099]<\/a> Fr\u00e9d\u00e9ric Loulergue, <\/br>Implementing Algorithmic Skeletons with Bulk Synchronous Parallel ML<\/strong><\/br>2017 18th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT)<\/i>, Dec 2017, Taipei, Taiwan. pp.461-468, ⟨10.1109\/PDCAT.2017.00079⟩<\/a><\/br><\/br>[hal-02317101]<\/a> Virginia Niculescu, Fr\u00e9d\u00e9ric Loulergue, Darius Bufnea, Adrian Sterca, <\/br>A Java Framework for High Level Parallel Programming Using Powerlists<\/strong><\/br>2017 18th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT)<\/i>, Dec 2017, Taipei, France. pp.255-262, ⟨10.1109\/PDCAT.2017.00049⟩<\/a><\/br><\/br>[hal-02317103]<\/a> Fr\u00e9d\u00e9ric Loulergue, <\/br>A BSPlib-style API for Bulk Synchronous Parallel ML<\/strong><\/br>Scalable Computing: Practice and Experience<\/i>, 2017, 18 (3), ⟨10.12694\/scpe.v18i3.1306⟩<\/a><\/br><\/br>[hal-02317113]<\/a> Fr\u00e9d\u00e9ric Loulergue, <\/br>Special Issue of Scalable Computing: Practice and Experience on Practical Aspects of High-Level Parallel Programming<\/strong><\/br>Scalable Computing: Practice and Experience<\/i>, 18 (1), 2017, Scalable Computing: Practice and Experience, ⟨10.12694\/scpe.v18i1.1229⟩<\/a><\/br><\/br>[hal-01495456]<\/a> Fr\u00e9d\u00e9ric Loulergue, <\/br>Imperative BSPlib-style Communications in Bulk Synchronous Parallel ML<\/strong><\/br>International Conference on Computational Science<\/i>, Jun 2017, Zurich, Switzerland. ⟨10.1016\/j.procs.2017.05.267⟩<\/a><\/br><\/br>[hal-02317096]<\/a> Fr\u00e9d\u00e9ric Loulergue, <\/br>A Verified Accumulate Algorithmic Skeleton<\/strong><\/br>2017 Fifth International Symposium on Computing and Networking (CANDAR)<\/i>, Nov 2017, Aomori, France. pp.420-426, ⟨10.1109\/CANDAR.2017.108⟩<\/a><\/br><\/br>[hal-01944569]<\/a> Jean-Michel Couvreur, Joaqu\u00edn Ezpeleta, <\/br>A Linear Temporal Logic Model Checking Method over Finite Words with Correlated Transition Attributes<\/strong><\/br>7th International Symposium on Data-Driven Process Discovery and Analysis (SIMPDA)<\/i>, Dec 2017, Neuch\u00e2tel, Switzerland. pp.89-104, ⟨10.1007\/978-3-030-11638-5_5⟩<\/a><\/br><\/br>[hal-01559832]<\/a> Frederic Dabrowski, <\/br>Textual Alignment in SPMD Programs<\/strong><\/br>[Research Report] RR-2017-07, LIFO, Universit\u00e9 d'Orl\u00e9ans. 2017<\/br><\/br>

2016<\/H2>[hal-01291393]<\/a> Yohan Boichut, Pierre R\u00e9ty, Vivien Pelletier, <\/br>Synchronized Tree Languages for Reachability in Non-right-linear Term Rewrite Systems<\/strong><\/br>International Workshop on Rewriting Logic and its Applications<\/i>, Apr 2016, Eindhoven, Netherlands<\/br><\/br>[hal-01318432]<\/a> Allan Blanchard, Nikolai Kosmatov, Fr\u00e9d\u00e9ric Loulergue, <\/br>A CHR-Based Solver for Weak Memory Behaviors<\/strong><\/br>7th Workshop on Constraint Solvers in Testing, Verification, and Analysis (CSTVA)<\/i>, Jul 2016, Saarbr\u00fccken, Germany<\/br><\/br>[hal-01423641]<\/a> Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Fr\u00e9d\u00e9ric Loulergue, <\/br>Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs<\/strong><\/br>2016 IEEE 16th International Working Conference on Source Code Analysis and Manipulation (SCAM)<\/i>, 2016, Raleigh, NC, United States. pp.6, ⟨10.1109\/SCAM.2016.18⟩<\/a><\/br><\/br>[hal-01319565]<\/a> Thibaut Tachon, Ga\u00e9tan Hains, Fr\u00e9d\u00e9ric Loulergue, Chong Li, <\/br>Automated generation of BSP automata<\/strong><\/br>High Level Parallel Programming and Applications (HLPP)<\/i>, Jul 2016, M\u00fcnster, Germany<\/br><\/br>

2015<\/H2>[hal-01107296]<\/a> Fr\u00e9d\u00e9ric Loulergue, Wadoud Bousdira, Julien Tesson, <\/br>Calcul de programmes parall\u00e8les avec Coq<\/strong><\/br>Informatique Math\u00e9matique<\/i>, CNRS \u00c9ditions<\/a>, 2015, collection Alpha<\/br><\/br>[hal-01143199]<\/a> Fr\u00e9d\u00e9ric Dabrowski, Fr\u00e9d\u00e9ric Loulergue, Thomas Pinsard, <\/br>A formal semantics of nested atomic sections with thread escape<\/strong><\/br>Computer Languages, Systems and Structures<\/i>, 2015, 42 (supl), pp.2-21. ⟨10.1016\/j.cl.2015.04.001⟩<\/a><\/br><\/br>[hal-01105093]<\/a> Fr\u00e9d\u00e9ric Dabrowski, Fr\u00e9d\u00e9ric Loulergue, Thomas Pinsard, <\/br>Nested atomic sections with thread escape: Compilation to threads and locks<\/strong><\/br>ACM Symposium on Applied Computing (SAC)<\/i>, Apr 2015, Salamanca, Spain<\/br><\/br>[hal-01225332]<\/a> Nirina Andrianarivelo, Pierre R\u00e9ty, <\/br>Over-Approximating Terms Reachable by Context-Sensitive Rewriting<\/strong><\/br>Reachability Problems - 9th International Workshop RP 2015<\/i>, Sep 2015, Varsaw, Poland<\/br><\/br>[hal-01135918]<\/a> Yohan Boichut, Jacques Chabin, Pierre R\u00e9ty, <\/br>Towards More Precise Rewriting Approximations<\/strong><\/br>Proceedings of Language and Automata Theory and Applications (LATA)<\/i>, Mar 2015, Nice, France<\/br><\/br>[hal-01158137]<\/a> Fr\u00e9d\u00e9ric Loulergue, <\/br>Construction de programmes parall\u00e8les en Coq avec des homomorphismes de listes<\/strong><\/br>14\u00e8mes journ\u00e9es Approches Formelles dans l'Assistance au D\u00e9veloppement Logiciel (AFADL)<\/i>, 2015, Bordeaux, France<\/br><\/br>[hal-01158134]<\/a> Asma Guesmi, Patrice Clemente, Fr\u00e9d\u00e9ric Loulergue, Pascal Berthom\u00e9, <\/br>Cloud Resources Placement Based on Functional and Non-Functional Requirements<\/strong><\/br>SECRYPT<\/i>, Jul 2015, Colmar, France<\/br><\/br>[cea-01834977]<\/a> Allan Blanchard, N. Kosmatov, M. Lemerre, Fr\u00e9d\u00e9ric Loulergue, <\/br>A case study on formal verification of the anaxagoros hypervisor paging system with frama-C<\/strong><\/br>FMICS 2015 - Formal Methods for Industrial Critical Systems<\/i>, Jun 2015, Oslo, Norway. pp.15-30, ⟨10.1007\/978-3-319-19458-5_2⟩<\/a><\/br><\/br>[hal-01158138]<\/a> Fr\u00e9d\u00e9ric Loulergue, <\/br>Mod\u00e8les fonctionnels de MapReduce en Coq<\/strong><\/br>Journ\u00e9es Nationales du GdR GPL<\/i>, 2015, Bordeaux, France<\/br><\/br>
<\/p>
<\/p>\n\n\n\n

<\/p>\n","protected":false},"excerpt":{"rendered":"","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":4,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-18","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages\/18","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/comments?post=18"}],"version-history":[{"count":7,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages\/18\/revisions"}],"predecessor-version":[{"id":51,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages\/18\/revisions\/51"}],"wp:attachment":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/media?parent=18"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}