Publications

2022


2021

Modular termination of prefix-constrained term rewrite systems
Information Processing Letters, Elsevier, 2021, pp.106207. ⟨10.1016/j.ipl.2021.106207⟩
Nirina Andrianarivelo, Pierre Réty,

An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2021, Volume 17, Issue 4, ⟨10.46298/lmcs-17(4:22)2021⟩
Jules Chouquet, Lionel Vaux,

Reflection on the Design of Parallel Programming Frameworks
Evaluation of Novel Approaches to Software Engineering, pp.154-181, 2021, ⟨10.1007/978-3-030-70006-5_7⟩
Virginia Niculescu, Frédéric Loulergue, Adrian Sterca,

Tests and Proofs
Springer, 2021, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-79379-1⟩
Frédéric Loulergue, Franz Wotawa,

Experience report: Teaching code analysis and verification using Frama-C
1st International Workshop on Applicable Formal Methods (appFM), Nov 2021, Beijing, China
Salwa Souaf, Frédéric Loulergue,

On Single-Valuedness in Textually Aligned SPMD Programs
International Journal of Parallel Programming, 2021, International Journal of Parallel Programming, ⟨10.1007/s10766-021-00710-5⟩
Frederic Dabrowski,


2020

Verified Runtime Assertion Checking for Memory Properties
TAP 2020 - 14th International Conference on Tests and Proofs, Jun 2020, Bergen, Norway. ⟨10.1007/978-3-030-50995-8_6⟩
Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles,

Transforming powerlist-based divide-and-conquer programs for an improved execution model
Journal of Supercomputing, Springer Verlag, 2020, 76 (7), pp.22. ⟨10.1007/s11227-019-02820-x⟩
Virginia Niculescu, Frédéric Loulergue,

Pattern-driven Design of a Multiparadigm Parallel Programming Framework
13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), 2020, Prague, Czech Republic
Virginia Niculescu, Frédéric Loulergue, Darius Bufnea, Adrian Sterca,

Special Issue of the Journal of Logical and Algebraic Methods in Programming on Formal Approaches to Parallel and Distributed Systems 2018
Journal of Logical and Algebraic Methods in Programming, 116, Elsevier, pp.100580, 2020, ⟨10.1016/j.jlamp.2020.100580⟩
Frédéric Loulergue,

Verification of DRMA communications
High-level Parallel Programming and Applications, Jul 2020, Porto, Portugal
Frederic Dabrowski,

The Journal of Supercomputing volume 76, page 4976 (2020)
2020
Frederic Dabrowski,


2019

Safe Usage of Registers in BSPlib
SAC 2019, Apr 2019, Limassol, Cyprus. ⟨10.1145/3297280.3297421⟩
Wadoud Bousdira, Arvid Jakobsson, Frederic Dabrowski,

Safe Usage of Registers in BSPlib (Preprint)
2019
Arvid Jakobsson, Frederic Dabrowski, Wadoud Bousdira,

Modeling Concurrent Behaviors as Words
Verification and Evaluation of Computer and Communication Systems, 11847, Springer International Publishing, pp.1-15, 2019, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-35092-5_1⟩
Yohan Boichut, Jean-Michel Couvreur, Xavier Ferry, Mohamadou Tafsir Sakho,

Soundness of a Dataflow Analysis for Memory Monitoring
Ada Letters, Association for Computing Machinery, 2019, 38 (2), pp.97-108. ⟨10.1145/3375408.3375416⟩
Dara Ly, Nikolai Kosmatov, Julien Signoles, Frédéric Loulergue,

Towards more precise rewriting approximations
Journal of Computer and System Sciences, Elsevier, 2019, 104, pp.131-148
Yohan Boichut, Jacques Chabin, Pierre Réty,

Transforming non textually aligned SPMD programs into textually aligned SPMD programs by using rewriting rules
IEEE/ACM International Conference on High Performance Computing & Simulation, Jul 2019, Dublin, Ireland. pp.982-989
Wadoud Bousdira,

Unification modulo Lists with Reverse, Relation with Certain Word Equations
CADE-27 - The 27th International Conference on Automated Deduction, Association for Automated Reasoning (AAR), Aug 2019, Natal, Brazil. pp.1--17, ⟨10.1007/978-3-030-29436-6_1⟩
Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michaël Rusinowitch,

Automatic Generation of Bulk-Synchronous Parallel code
Distributed, Parallel, and Cluster Computing [cs.DC]. Université d'Orléans, 2019. English. ⟨NNT : 2019ORLE3098⟩
Thibaut Tachon,

Unification modulo Lists with Reverse as Solving Simple Sets of Word Equations
[Research Report] LIFO, Université d'Orléans; INSA, Centre Val de Loire. 2019
Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michael Rusinowitch,

Static Analysis for BSPlib Programs
Distributed, Parallel, and Cluster Computing [cs.DC]. Université d'Orléans, 2019. English. ⟨NNT : 2019ORLE2005⟩
Filip Jakobsson,

Parallel programming with Coq: Map and reduce skeletons on trees
34th ACM/SIGAPP Symposium on Applied Computing (SAC), Apr 2019, Limassol, Cyprus. pp.1578-1581, ⟨10.1145/3297280.3299742⟩
Jolan Philippe, Frédéric Loulergue,

Towards Full Proof Automation in Frama-C Using Auto-active Verification
NFM 2019 - 11th Annual NASA Formal Methods Symposium, May 2019, Houston, TX, United States. pp.88-105, ⟨10.1007/978-3-030-20652-9_6⟩
Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov,

La logique contre les fantômes: comparaison de deux approches pour la preuve d'un module de listes chaînées *
18e journées Approches Formelles dans l'Assistance au Développement de Logic (AFADL), Jun 2019, Toulouse, France
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,

PySke: Algorithmic Skeletons for Python
The 2019 International Conference on High Performance Computing & Simulation (HPCS), Jul 2019, Dublin, Ireland. ⟨10.1109/HPCS48598.2019.9188151⟩
Jolan Philippe, Frédéric Loulergue,

A First Step in the Translation of Alloy to Coq
21st International Conference on Formal Engineering Methods (ICFEM), 2019, Shenzen, China. ⟨10.1007/978-3-030-32409-4_28⟩
Salwa Souaf, Frédéric Loulergue,

Towards automatically optimizing PySke programs (poster)
International Conference on High Performance Computing and Simulation (HPCS), Jul 2019, Dublin, Ireland. ⟨10.1109/HPCS48598.2019.9188160⟩
Jolan Philippe, Frédéric Loulergue,

Logic against Ghosts: Comparison of Two Proof Approaches for a List Module
SAC 2019 - The 34th ACM/SIGAPP Symposium On Applied Computing, Apr 2019, Limassol, Cyprus. ⟨10.1145/3297280.3297495⟩
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,

Automatic Optimization of Python Skeletal Parallel Programs
19th International Conference on Algorithms and Architectures for Parallel Processing (ICA3PP), Dec 2019, Melbourne, Australia. ⟨10.1007/978-3-030-38991-8_13⟩
Frédéric Loulergue, Jolan Philippe,

New List Skeletons for the Python Skeleton Library
PDCAT 2019: 20th International Conference on Parallel and Distributed Computing, Applications and Technologies, Dec 2019, Gold Coast, Australia. ⟨10.1109/PDCAT46702.2019.00077⟩
Frédéric Loulergue, Jolan Philippe,

A denotational semantics of textually aligned SPMD Program
Journal of Logical and Algebraic Methods in Programming, Elsevier, 2019, ⟨10.1016/j.jlamp.2019.02.010⟩
Frederic Dabrowski,


2018

Approximating any Logic Program by a CS-Program
Rewriting Logic and Its Applications - 12th International Workshop, Apr 2018, Thessalonique, Greece. pp.245--260
Yohan Boichut, Vivien Pelletier, Pierre Rety,

Confluence of Prefix-Constrained Rewrite Systems
3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Jul 2018, Oxford, United Kingdom
Nirina Andrianarivelo, Pierre Rety,

Automatic Cost Analysis for Imperative BSP Programs
International Journal of Parallel Programming, Springer Verlag, 2018, ⟨10.1007/s10766-018-0562-1⟩
Arvid Jakobsson,

Towards formal methods and software engineering for deep learning: Security, safety and productivity for dl systems development
2018 Annual IEEE International Systems Conference (SysCon), Apr 2018, Vancouver, France. ⟨10.1109/SYSCON.2018.8369576⟩
Gaétan Hains, Arvid Jakobsson, Youry Khmelevsky,

Soundness of a Dataflow Analysis for Memory Monitoring
HILT 2018 Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems, Nov 2018, Boston, United States. ⟨10.1145/3375408.3375416⟩
Dara Ly, Nikolai Kosmatov, Julien Signoles, Frédéric Loulergue,

A Denotational Semantics of Textually Aligned SPMD Programs
International Conference on High Performance Computing & Simulation, Jul 2018, Orléans, France. ⟨10.1109/HPCS.2018.00119⟩
Frédéric Dabrowski,

Textual Alignment in SPMD Programs
SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing, Apr 2018, Pau, France. ⟨10.1145/3167132.3167254⟩
Frederic Dabrowski,

Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C
Tenth NASA Formal Methods Symposium - NFM 2018, Apr 2018, Newport News, United States. ⟨10.1007/978-3-319-77935-5_3⟩
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,

A Lesson on Verification of IoT Software with Frama-C
2018 International Conference on High Performance Computing & Simulation (HPCS), Jul 2018, Orleans, France. pp.21-30, ⟨10.1109/HPCS.2018.00018⟩
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,

Des listes et leurs fantômes : vérification d'un module critique de Contiki avec FRAMA-C
17èmes Journées AFADL : Approches Formelles Dans L'assistance Au Développement De Logiciels, Jun 2018, Toulouse, France
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,

MMFilter: A CHR-Based Solver for Generation of Executions under Weak Memory Models
Computer Languages, Systems and Structures, Elsevier, 2018, 53, pp.121-142. ⟨10.1016/j.cl.2018.03.002⟩
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,

Ghosts for Lists: from Axiomatic to Executable Specifications
TAP 2018 - 12th International Conference on Tests and Proofs, Jun 2018, Toulouse, France. ⟨10.1007/978-3-319-92994-1_11⟩
Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov,


2017

Replicated Synchronization for Imperative BSP Programs
International Conference on Computational Science (ICCS), 2017, Zürich, Switzerland. ⟨10.1016/j.procs.2017.05.123⟩
Arvid Jakobsson, Frederic Dabrowski, Wadoud Bousdira, Frédéric Loulergue, Gaetan Hains,

Formalization of a Big Graph API in Coq
2017 International Conference on High Performance Computing & Simulation (HPCS), Jul 2017, Genoa, France. IEEE, 108, pp.893-894, 2017, ⟨10.1109/HPCS.2017.140⟩
Jolan Philippe, Wadoud Bousdira, Frédéric Loulergue,

Calculating Parallel Programs in Coq using List Homomorphisms
International Journal of Parallel Programming, Springer Verlag, 2017, 45 (2), pp.300-319. ⟨10.1007/s10766-016-0415-8⟩
Frédéric Loulergue, Wadoud Bousdira, Julien Tesson,

Automated generation of BSP automata
Parallel Processing Letters, World Scientific Publishing, 2017, 17 (1), ⟨10.1142/S0129626417400023⟩
Thibaut Tachon, Chong Li, Gaétan Hains, Frédéric Loulergue,

From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
Fifth International Workshop on Verification and Program Transformation (VPT 2017), Apr 2017, Uppsala, Sweden. ⟨10.4204/EPTCS.253.9⟩
Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov,

Transforming Prefix-Constrained or Controlled Rewrite Systems
8th International Symposium on Symbolic Computation in Software Science (SCSS 2017), Apr 2017, Gammarth, Tunisia
Nirina Andrianarivelo, Vivien Pelletier, Pierre Réty,

A Java Framework for High Level Parallel Programming Using Powerlists
2017 18th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT), Dec 2017, Taipei, France. pp.255-262, ⟨10.1109/PDCAT.2017.00049⟩
Virginia Niculescu, Frédéric Loulergue, Darius Bufnea, Adrian Sterca,

Special Issue of Scalable Computing: Practice and Experience on Practical Aspects of High-Level Parallel Programming
Scalable Computing: Practice and Experience, 18 (1), 2017, Scalable Computing: Practice and Experience, ⟨10.12694/scpe.v18i1.1229⟩
Frédéric Loulergue,

Towards a Verified Parallel Implementation of Frequent Itemset Mining
2017 International Conference on High Performance Computing & Simulation (HPCS), Jul 2017, Genoa, Italy. IEEE, pp.889-890, ⟨10.1109/HPCS.2017.138⟩
Christopher Whitney, Frédéric Loulergue,

A BSPlib-style API for Bulk Synchronous Parallel ML
Scalable Computing: Practice and Experience, 2017, 18 (3), ⟨10.12694/scpe.v18i3.1306⟩
Frédéric Loulergue,

Implementing Algorithmic Skeletons with Bulk Synchronous Parallel ML
2017 18th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT), Dec 2017, Taipei, Taiwan. pp.461-468, ⟨10.1109/PDCAT.2017.00079⟩
Frédéric Loulergue,

A Verified Accumulate Algorithmic Skeleton
2017 Fifth International Symposium on Computing and Networking (CANDAR), Nov 2017, Aomori, France. pp.420-426, ⟨10.1109/CANDAR.2017.108⟩
Frédéric Loulergue,

Imperative BSPlib-style Communications in Bulk Synchronous Parallel ML
International Conference on Computational Science, Jun 2017, Zurich, Switzerland. ⟨10.1016/j.procs.2017.05.267⟩
Frédéric Loulergue,

A Linear Temporal Logic Model Checking Method over Finite Words with Correlated Transition Attributes
7th International Symposium on Data-Driven Process Discovery and Analysis (SIMPDA), Dec 2017, Neuchâtel, Switzerland. pp.89-104, ⟨10.1007/978-3-030-11638-5_5⟩
Jean-Michel Couvreur, Joaquín Ezpeleta,

Textual Alignment in SPMD Programs
[Research Report] RR-2017-07, LIFO, Université d'Orléans. 2017
Frederic Dabrowski,


2016

Synchronized Tree Languages for Reachability in Non-right-linear Term Rewrite Systems
International Workshop on Rewriting Logic and its Applications, Apr 2016, Eindhoven, Netherlands
Yohan Boichut, Pierre Réty, Vivien Pelletier,

A CHR-Based Solver for Weak Memory Behaviors
7th Workshop on Constraint Solvers in Testing, Verification, and Analysis (CSTVA), Jul 2016, Saarbrücken, Germany
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,

Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs
2016 IEEE 16th International Working Conference on Source Code Analysis and Manipulation (SCAM), 2016, Raleigh, NC, United States. pp.6, ⟨10.1109/SCAM.2016.18⟩
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue,

Automated generation of BSP automata
High Level Parallel Programming and Applications (HLPP), Jul 2016, Münster, Germany
Thibaut Tachon, Gaétan Hains, Frédéric Loulergue, Chong Li,


2015

Calcul de programmes parallèles avec Coq
Informatique Mathématique, CNRS Éditions, 2015, collection Alpha
Frédéric Loulergue, Wadoud Bousdira, Julien Tesson,

Nested atomic sections with thread escape: Compilation to threads and locks
ACM Symposium on Applied Computing (SAC), Apr 2015, Salamanca, Spain
Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard,

A formal semantics of nested atomic sections with thread escape
Computer Languages, Systems and Structures, Elsevier, 2015, 42 (supl), pp.2-21. ⟨10.1016/j.cl.2015.04.001⟩
Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard,

Over-Approximating Terms Reachable by Context-Sensitive Rewriting
Reachability Problems - 9th International Workshop RP 2015, Sep 2015, Varsaw, Poland
Nirina Andrianarivelo, Pierre Réty,

Towards More Precise Rewriting Approximations
Proceedings of Language and Automata Theory and Applications (LATA), Mar 2015, Nice, France
Yohan Boichut, Jacques Chabin, Pierre Réty,

Cloud Resources Placement Based on Functional and Non-Functional Requirements
SECRYPT, Jul 2015, Colmar, France
Asma Guesmi, Patrice Clemente, Frédéric Loulergue, Pascal Berthomé,

A case study on formal verification of the anaxagoros hypervisor paging system with frama-C
FMICS 2015 - Formal Methods for Industrial Critical Systems, Jun 2015, Oslo, Norway. pp.15-30, ⟨10.1007/978-3-319-19458-5_2⟩
Allan Blanchard, N. Kosmatov, M. Lemerre, Frédéric Loulergue,

Construction de programmes parallèles en Coq avec des homomorphismes de listes
14èmes journées Approches Formelles dans l'Assistance au Développement Logiciel (AFADL), 2015, Bordeaux, France
Frédéric Loulergue,

Modèles fonctionnels de MapReduce en Coq
Journées Nationales du GdR GPL, 2015, Bordeaux, France
Frédéric Loulergue,