Publications

Publications HAL du labo/EPI SYCOMORES

2024

Journal articles

titre
Formal Definitions and Proofs for Partial (Co)Recursive Functions
auteur
Horatiu Cheval, David Nowak, Vlad Rusu
article
Journal of Logic and Algebraic Methods in Programming, 2024, 141, pp.27. ⟨10.1016/j.jlamp.2024.100999⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04360660/file/jlamp.pdf BibTex
titre
Parametric WCET as a function of procedure arguments: analysis and applications
auteur
Sandro Grebant, Clément Ballabriga, Julien Forget, Giuseppe Lipari
article
Journal of Systems Architecture, 2024, 148, ⟨10.1016/j.sysarc.2024.103086⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04433439/file/grebant2024-parametric.pdf BibTex

Conference papers

titre
A Linear Type System for Lp-Metric Sensitivity Analysis
auteur
Victor Sannier, Patrick Baillot
article
Formal Structures for Computation and Deduction (FSCD), Jul 2024, Tallinn, Estonia. pp.12:1–12:22, ⟨10.4230/LIPIcs.FSCD.2024.12⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04514677/file/plurimetric-fuzz-article.pdf BibTex
titre
Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)
auteur
Raphaël Monat, Marco Milanese, Francesco Parolini, Jérôme Boillot, Abdelraouf Ouadjaout, Antoine Miné
article
Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024, Apr 2024, Luxembourg City, Luxembourg. pp.387 – 392, ⟨10.1007/978-3-031-57256-2_26⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04536418/file/978-3-031-57256-2_26.pdf BibTex
titre
On Basic Feasible Functionals and the Interpretation Method
auteur
Patrick Baillot, Ugo Dal Lago, Cynthia Kop, Deivid Vale
article
FoSSaCS 2024 – 27th International Conference on Foundations of Software Science and Computation Structures, Apr 2024, Luxembourg, Luxembourg. pp.70-91, ⟨10.1007/978-3-031-57231-9_4⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04743265/file/paper_basicFeasibleFunctionals.pdf BibTex
titre
Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law
auteur
Raphaël Monat, Aymeric Fromherz, Denis Merigoux
article
ESOP 2024 – 33rd European Symposium on Programming, Apr 2024, Luxembourg City, Luxembourg. pp.421-450, ⟨10.1007/978-3-031-57267-8_16⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04536403/file/978-3-031-57267-8_16.pdf BibTex

Preprints, Working Papers, …

titre
Easing Maintenance of Academic Static Analyzers
auteur
Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné
article
2024
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04652657/file/sttt_mopsa_maintenance-revised.pdf BibTex
titre
Session Types for the Concurrent Composition of Interactive Differential Privacy
auteur
Victor Sannier, Patrick Baillot, Marco Gaboardi
article
2024
Accès au texte intégral et bibtex
https://hal.science/hal-04719333/file/concomp-article.pdf BibTex
titre
A Kleene algebra with tests for union bound reasoning about probabilistic programs
auteur
Leandro Gomes, Patrick Baillot, Marco Gaboardi
article
2024
Accès au texte intégral et bibtex
https://hal.science/hal-04196675/file/aGKAT_HAL_july2024.pdf BibTex

2023

Journal articles

titre
From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact)
auteur
Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, Susanne Graf, J. Javier Gutiérrez, Rafik Henia, Didier Le Botlan, Giuseppe Lipari, Julio Medina, Nicolas Navet, Sophie Quinton, Juan Rivas, Youcheng Sun
article
Dagstuhl Artifacts Series, 2023, 9 (1), ⟨10.4230/DARTS.9.1.4⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04254710/file/DARTS.9.1.4.pdf BibTex

Conference papers

titre
While Loops in Coq
auteur
David Nowak, Vlad Rusu
article
7th Symposium on Working Formal Methods (FROM 2023), Sep 2023, Bucarest, Romania. pp.96 – 109, ⟨10.4204/eptcs.389.8⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04254872/file/paper.pdf BibTex
titre
From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Invited Paper)
auteur
Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, Susanne Graf, J. Javier Gutiérrez, Rafik Henia, Didier Le Botlan, Giuseppe Lipari, Julio Medina, Nicolas Navet, Sophie Quinton, Juan Rivas, Youcheng Sun
article
35th Euromicro Conference on Real-Time Systems (ECRTS 2023), Jul 2023, Vienne, Austria. ⟨10.4230/LIPIcs.ECRTS.2023.19⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04654624/file/From%20FMTV%20to%20WATERS.pdf BibTex
titre
New challenges in adaptive real-time systems with parametric WCET
auteur
Clément Ballabriga, Julien Forget, Sandro Grebant, Giuseppe Lipari
article
RTSOPS 2023 – 12th International Real-Time Scheduling Open Problems Seminar, Jul 2023, Vienne, Austria
Accès au texte intégral et bibtex
https://hal.science/hal-04197411/file/forget-rtsops2023.pdf BibTex
titre
WCET analysis with procedure arguments as parameters
auteur
Sandro Grebant, Clément Ballabriga, Julien Forget, Giuseppe Lipari
article
RTNS 2023: The 31st International Conference on Real-Time Networks and Systems, Jun 2023, Dortmund, Germany. pp.11-22, ⟨10.1145/3575757.3593655⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04118213/file/main.pdf BibTex
titre
Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution)
auteur
Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné
article
Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Apr 2023, Paris, France. pp.565-570, ⟨10.1007/978-3-031-30820-8_37⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04077678/file/978-3-031-30820-8_37.pdf BibTex
titre
Bunched Fuzz: Sensitivity for Vector Metrics
auteur
June Wunder, Arthur Azevedo De Amorim, Patrick Baillot, Marco Gaboardi
article
ESOP 2023 – European Symposium on Programming, Apr 2023, Paris, France. ⟨10.48550/arXiv.2202.01901⟩
Accès au bibtex
https://arxiv.org/pdf/2202.01901 BibTex
titre
Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs
auteur
Milla Valnet, Raphaël Monat, Antoine Miné
article
JFLA 2023 – 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.211-242
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03936718/file/jfla23_paper_4105_v2.pdf BibTex

Theses

titre
Processor and memory co-scheduling of embedded real-time applications on multicore platforms
auteur
Ikram Senoussaoui
article
Distributed, Parallel, and Cluster Computing [cs.DC]. Université de Lille; Université Oran 1 (Algérie), 2023. English. ⟨NNT : 2023ULILB051⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-04495150/file/These_SENOUSSAOUI_Ikram.pdf BibTex
titre
Efficient tree-based symbolic WCET computation
auteur
Sandro Grebant
article
Data Structures and Algorithms [cs.DS]. Université de Lille, 2023. English. ⟨NNT : 2023ULILB028⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-04394652/file/These_GREBANT_Sandro.pdf BibTex

Preprints, Working Papers, …

titre
BiGKAT: an algebraic framework for relational verification of probabilistic programs
auteur
Leandro Gomes, Patrick Baillot, Marco Gaboardi
article
2023
Accès au texte intégral et bibtex
https://hal.science/hal-04017128/file/BiGKAT_techreport.pdf BibTex

2022

Journal articles

titre
Reducing the fault vulnerability of hard real-time systems
auteur
Fabien Bouquillon, Smail Niar, Giuseppe Lipari
article
Journal of Systems Architecture, 2022, 133, pp.102758. ⟨10.1016/j.sysarc.2022.102758⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03842393/file/main.pdf BibTex
titre
Relational abstract interpretation of arrays in assembly code
auteur
Clément Ballabriga, Julien Forget, Jordy Ruiz
article
Formal Methods in System Design, 2022, ⟨10.1007/s10703-022-00399-3⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03794951/file/ballabriga-et-al-2022-accepted.pdf BibTex
titre
A Linux-Based Support for Developing Real-Time Applications on Heterogeneous Platforms with Dynamic FPGA Reconfiguration
auteur
Marco Pagani, Alessandro Biondi, Mauro Marinoni, Lorenzo Molinari, Giuseppe Lipari, Giorgio Buttazzo
article
Future Generation Computer Systems, 2022, 129, pp.125-140. ⟨10.1016/j.future.2021.11.007⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03512476/file/fredlinux-journal.pdf BibTex
titre
Memory-processor co-scheduling for real-time tasks on network-on-chip manycore architectures
auteur
Chawki Benchehida, Mohammed Kamel Benhaoua, Houssam Zahaf, Giuseppe Lipari
article
International Journal of High Performance Systems Architecture (IJHPSA), 2022, 11 (1), pp.1-11. ⟨10.1504/IJHPSA.2022.121877⟩
Accès au texte intégral et bibtex
https://cnrs.hal.science/hal-03595577/file/main.pdf BibTex

Conference papers

titre
Toward memory-centric scheduling for PREM task on multicore platforms, when processor assignments are specified
auteur
Ikram Senoussaoui, Mohammed Kamel Benhaoua, Houssam-Eddine Zahaf, Giuseppe Lipari
article
EDiS 2022 – 3rd International Conference on Embedded & Distributed Systems, Nov 2022, Oran, France. pp.11-15, ⟨10.1109/EDiS57230.2022.9996534⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03938665/file/EDiS2022_paper.pdf BibTex
titre
Contention-free scheduling of PREM tasks on partitioned multicore platforms
auteur
Ikram Senoussaoui, Houssam-Eddine Zahaf, Giuseppe Lipari, Kamel Benhaoua
article
2022 IEEE 27th International Conference on Emerging Technologies and Factory Automation (ETFA), Sep 2022, Stuttgart, Germany
Accès au texte intégral et bibtex
https://hal.science/hal-03834177/file/main.pdf BibTex
titre
Defining Corecursive Functions in Coq Using Approximations
auteur
Vlad Rusu, David Nowak
article
ECOOP, Jun 2022, Berlin, Germany. ⟨10.4230/LIPIcs.ECOOP.2022.12⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03671876/file/final.pdf BibTex
titre
A Formal Correctness Proof for an EDF Scheduler Implementation
auteur
Florian Vanhems, Vlad Rusu, David Nowak, Gilles Grimaud
article
RTAS 2022: 28th IEEE Real-Time and Embedded Technology and Applications Symposium, May 2022, Milan, Italy. ⟨10.1109/RTAS54340.2022.00030⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03671598/file/edf_paper.pdf BibTex
titre
Synchronous semantics of multi-mode multi-periodic systems
auteur
Frédéric Fort, Julien Forget
article
SAC ’22: The 37th ACM/SIGAPP Symposium on Applied Computing, Apr 2022, Virtual Event, France. pp.1248-1257, ⟨10.1145/3477314.3507271⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03817684/file/main.pdf BibTex
titre
Improving CRPD Analysis for EDF Scheduling: Trading Speed for Precision
auteur
Giuseppe Lipari, Fabien Bouquillon, Smail Niar
article
The 37th ACM/SIGAPP Symposium On Applied Computing, Apr 2022, Brno, Czech Republic. ⟨10.1145/3477314.3507027⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03531143/file/preempt-interval.pdf BibTex

Proceedings

titre
Working Formal Methods Symposium
auteur
Vlad Rusu
article
FROM’22, Electronic Proceedings in Theoretical Computer Science, 369, 2022, ⟨10.4204/EPTCS.369⟩
Accès au bibtex
BibTex

Theses

titre
Improving the reliability of heterogeneous multicore architecture for intelligent transportation systems
auteur
Fabien Bouquillon
article
Embedded Systems. Université de Lille, 2022. English. ⟨NNT : 2022ULILB021⟩
Accès au texte intégral et bibtex
https://hal.science/tel-03895529/file/These_BOUQUILLON_Fabien.pdf BibTex
titre
Programing adaptive real-time systems
auteur
Frédéric Fort
article
Programming Languages [cs.PL]. Université de Lille, 2022. English. ⟨NNT : 2022ULILB024⟩
Accès au texte intégral et bibtex
https://hal.science/tel-03948472/file/These_FORT_Frederic.pdf BibTex

Preprints, Working Papers, …

titre
Towards Corecursion Without Corecursion in Coq
auteur
Vlad Rusu, David Nowak
article
2022
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03689027/file/wpte2022.pdf BibTex

2021

Journal articles

titre
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic
auteur
Vlad Rusu, David Nowak
article
Journal of Logical and Algebraic Methods in Programming, 2021, 118, ⟨10.1016/j.jlamp.2020.100619⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02978080/file/jlamp.pdf BibTex

2020

Software

titre
pip_edf_scheduler
auteur
Gilles Grimaud, David Nowak, Vlad Rusu, Florian Vanhems
article
2020, ⟨swh:1:dir:25301689cda60e938ba55243da1bfe7137563b79;origin=https://hal.archives-ouvertes.fr/hal-04429830;visit=swh:1:snp:3736179f223a1f39b86a1d803c559b4f4b76ffd6;anchor=swh:1:rel:759571c7c5be6020911ce733a23ead06b5884787;path=/⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04429830/file/pip_edf_scheduler-v1.0.0.zip BibTex

Comments are closed.