2018
Approximating any Logic Program by a CS-ProgramRewriting Logic and Its Applications - 12th International Workshop, Apr 2018, Thessalonique, Greece. pp.245--260Yohan Boichut, Vivien Pelletier, Pierre Rety,
Confluence of Prefix-Constrained Rewrite Systems3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Jul 2018, Oxford, United KingdomNirina Andrianarivelo, Pierre Rety,
Automatic Cost Analysis for Imperative BSP ProgramsInternational Journal of Parallel Programming, 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 development2018 Annual IEEE International Systems Conference (SysCon), Apr 2018, Vancouver, France.
⟨10.1109/SYSCON.2018.8369576⟩Gaétan Hains, Arvid Jakobsson, Youry Khmelevsky,
A Denotational Semantics of Textually Aligned SPMD ProgramsInternational Conference on High Performance Computing & Simulation, Jul 2018, Orléans, France.
⟨10.1109/HPCS.2018.00119⟩Frédéric Dabrowski,
Textual Alignment in SPMD ProgramsSAC '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-CTenth 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-C2018 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,
Ghosts for Lists: from Axiomatic to Executable SpecificationsTAP 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,
MMFilter: A CHR-Based Solver for Generation of Executions under Weak Memory ModelsComputer Languages, Systems and Structures, 2018, 53, pp.121-142.
⟨10.1016/j.cl.2018.03.002⟩Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,
Des listes et leurs fantômes : vérification d'un module critique de Contiki avec FRAMA-C17èmes Journées AFADL : Approches Formelles Dans L'assistance Au Développement De Logiciels, Jun 2018, Toulouse, FranceAllan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,
2017
Replicated Synchronization for Imperative BSP ProgramsInternational 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 Coq2017 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,
Transforming Prefix-Constrained or Controlled Rewrite Systems8th International Symposium on Symbolic Computation in Software Science (SCSS 2017), Apr 2017, Gammarth, TunisiaNirina Andrianarivelo, Vivien Pelletier, Pierre Réty,
Calculating Parallel Programs in Coq using List HomomorphismsInternational Journal of Parallel Programming, 2017, 45 (2), pp.300-319.
⟨10.1007/s10766-016-0415-8⟩Frédéric Loulergue, Wadoud Bousdira, Julien Tesson,
Automated generation of BSP automataParallel Processing Letters, 2017, 17 (1),
⟨10.1142/S0129626417400023⟩Thibaut Tachon, Chong Li, Gaétan Hains, Frédéric Loulergue,
A Linear Temporal Logic Model Checking Method over Finite Words with Correlated Transition Attributes7th 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. 2017Frederic Dabrowski,
From Concurrent Programs to Simulating Sequential Programs: Correctness of a TransformationFifth 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,
2016
Synchronized Tree Languages for Reachability in Non-right-linear Term Rewrite SystemsInternational Workshop on Rewriting Logic and its Applications, Apr 2016, Eindhoven, NetherlandsYohan Boichut, Pierre Réty, Vivien Pelletier,
A CHR-Based Solver for Weak Memory Behaviors7th Workshop on Constraint Solvers in Testing, Verification, and Analysis (CSTVA), Jul 2016, Saarbrücken, GermanyAllan Blanchard, Nikolai Kosmatov, Frédéric Loulergue,
Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs2016 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 automataHigh Level Parallel Programming and Applications (HLPP), Jul 2016, Münster, GermanyThibaut Tachon, Gaétan Hains, Frédéric Loulergue, Chong Li,
2015
Calcul de programmes parallèles avec CoqInformatique Mathématique,
CNRS Éditions, 2015, collection AlphaFrédéric Loulergue, Wadoud Bousdira, Julien Tesson,
A formal semantics of nested atomic sections with thread escapeComputer Languages, Systems and Structures, 2015, 42 (supl), pp.2-21.
⟨10.1016/j.cl.2015.04.001⟩Frédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard,
Nested atomic sections with thread escape: Compilation to threads and locksACM Symposium on Applied Computing (SAC), Apr 2015, Salamanca, SpainFrédéric Dabrowski, Frédéric Loulergue, Thomas Pinsard,
Over-Approximating Terms Reachable by Context-Sensitive RewritingReachability Problems - 9th International Workshop RP 2015, Sep 2015, Varsaw, PolandNirina Andrianarivelo, Pierre Réty,
Towards More Precise Rewriting ApproximationsProceedings of Language and Automata Theory and Applications (LATA), Mar 2015, Nice, FranceYohan Boichut, Jacques Chabin, Pierre Réty,
Cloud Resources Placement Based on Functional and Non-Functional RequirementsSECRYPT, Jul 2015, Colmar, FranceAsma Guesmi, Patrice Clemente, Frédéric Loulergue, Pascal Berthomé,
Construction de programmes parallèles en Coq avec des homomorphismes de listes14èmes journées Approches Formelles dans l'Assistance au Développement Logiciel (AFADL), 2015, Bordeaux, FranceFrédéric Loulergue,
A case study on formal verification of the anaxagoros hypervisor paging system with frama-CFMICS 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,
Modèles fonctionnels de MapReduce en CoqJournées Nationales du GdR GPL, 2015, Bordeaux, FranceFrédéric Loulergue,