Matthieu Lemerre

38 papers A* 1A 4B 7C 4Journal 11Unranked 10

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Relational Abstractions Based on Labeled Union-Find. Proc. ACM Program. Lang. Dorian Lesbre, Matthieu Lemerre, Hichem Rami Ait El Hara, François Bobot
2024	J	`jnl`	A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code. Proc. ACM Program. Lang. Julien Simonnet, Matthieu Lemerre, Mihaela Sighireanu
2024	J	`jnl`	Compiling with Abstract Interpretation. Proc. ACM Program. Lang. Dorian Lesbre, Matthieu Lemerre
2024	B	`conf`	Trace Partitioning as an Optimization Problem. SAS M. Charles Babu, Matthieu Lemerre, Sébastien Bardin, Jean-Yves Marion
2023	B	`conf`	Reverse Template Processing Using Abstract Interpretation. SAS Matthieu Lemerre
2023	J	`jnl`	SSA Translation Is an Abstract Interpretation. Proc. ACM Program. Lang. Matthieu Lemerre
2022	B	`conf`	Lightweight Shape Analysis Based on Physical Types. VMCAI Olivier Nicole, Matthieu Lemerre, Xavier Rival
2021	J	`jnl`	A relational shape abstract domain. Formal Methods Syst. Des. Hugo Illous, Matthieu Lemerre, Xavier Rival
2021	A*	`conf`	Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine. ICSE Frédéric Recoules, Sébastien Bardin, Richard Bonichon, Matthieu Lemerre, Laurent Mounier, Marie-Laure Potet
2021	J	`jnl`	Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine. CoRR Frédéric Recoules, Sébastien Bardin, Richard Bonichon, Matthieu Lemerre, Laurent Mounier, Marie-Laure Potet
2021	A	`conf`	No Crash, No Exploit: Automated Verification of Embedded Kernels. RTAS Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival
2021	—	`conf`	RUSTInA: Automatically Checking and Patching Inline Assembly Interface Compliance (Artifact Evaluation): Accepted submission #992 - "Interface Compliance of Inline Assembly: Automatically Check, Patch and Refine". ICSE (Companion Volume) Frédéric Recoules, Sébastien Bardin, Richard Bonichon, Matthieu Lemerre, Laurent Mounier, Marie-Laure Potet
2020	J	`jnl`	Automatically Proving Microkernels Free from Privilege Escalation from their Executable. CoRR Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival
2020	A	`conf`	Binary-level Directed Fuzzing for Use-After-Free Vulnerabilities. RAID Manh-Dung Nguyen, Sébastien Bardin, Richard Bonichon, Roland Groz, Matthieu Lemerre
2020	J	`jnl`	Binary-level Directed Fuzzing for Use-After-Free Vulnerabilities. CoRR Manh-Dung Nguyen, Sébastien Bardin, Richard Bonichon, Roland Groz, Matthieu Lemerre
2020	B	`conf`	Detection of Polluting Test Objectives for Dataflow Criteria. IFM Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, Matthieu Lemerre
2020	B	`conf`	Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries. SAS Hugo Illous, Matthieu Lemerre, Xavier Rival
2020	J	`jnl`	No Crash, No Exploit: Automated Verification of Embedded Kernels. CoRR Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, Xavier Rival
2018	B	`conf`	Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing. LPAR Benjamin Farinier, Robin David, Sébastien Bardin, Matthieu Lemerre
2017	—	`conf`	A Relational Shape Abstract Domain. NFM Hugo Illous, Matthieu Lemerre, Xavier Rival
2017	J	`jnl`	Abstract Interpretation using a Language of Symbolic Approximation. CoRR Matthieu Lemerre, Sébastien Bardin
2016	C	`conf`	Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs. SCAM Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
2016	C	`conf`	Proving Determinacy of the PharOS Real-Time Operating System. ABZ Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz
2015	C	`conf`	A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C. FMICS Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
2015	B	`conf`	Gamifying Program Analysis. LPAR Daniel Fava, Julien Signoles, Matthieu Lemerre, Martin Schäf, Ashish Tiwari
2015	C	`conf`	State Space Reduction Strategie for Model Checking Concurrent C Programs. VECoS Amira Methni, Matthieu Lemerre, Belgacem Ben Hedia, Serge Haddad, Kamel Barkaoui
2014	—	`conf`	A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing. TAP@STAF Nikolai Kosmatov, Matthieu Lemerre, Céline Alec
2014	—	`conf`	Specifying and Verifying Concurrent C Programs with TLA+. FTSCS Amira Methni, Matthieu Lemerre, Belgacem Ben Hedia, Serge Haddad, Kamel Barkaoui
2012	A	`conf`	A Model of Parallel Deterministic Real-Time Computation. RTSS Matthieu Lemerre, Emmanuel Ohayon
2012	J	`jnl`	Paravirtualizing Linux in a real-time hypervisor. SIGBED Rev. Vincent Legout, Matthieu Lemerre
2012	—	`conf`	Towards verified cloud computing environments. HPCS Frédéric Loulergue, Frédéric Gava, Nikolai Kosmatov, Matthieu Lemerre
2011	—	`conf`	Method and Tools for Mixed-Criticality Real-Time Applications within PharOS. ISORC Workshops Matthieu Lemerre, Emmanuel Ohayon, Damien Chabrol, Mathieu Jan, Marie-Bénédicte Jacques
2011	—	`conf`	The OASIS Kernel: A Framework for High Dependability Real-Time Systems. HASE Stéphane Louise, Matthieu Lemerre, Christophe Aussaguès, Vincent David
2010	—	`conf`	An Introduction to Time-Constrained Automata ICE Matthieu Lemerre, Vincent David, Christophe Aussaguès, Guy Vidal-Naquet
2010	—	`conf`	CONFIGEN: A tool for managing configuration options LoCoCo Emmanuel Ohayon, Matthieu Lemerre, Vincent David
2009	—	`conf`	A communication mechanism for resource isolation. IIES@EuroSys Matthieu Lemerre, Vincent David, Guy Vidal-Naquet
2009	—	`—`	Intégration de systèmes hétérogènes en termes de niveaux de sécurité. (Integration of systems with heterogeneous security levels). Matthieu Lemerre
2008	A	`conf`	Equivalence between Schedule Representations: Theory and Applications. IEEE Real-Time and Embedded Technology and Applications Symposium Matthieu Lemerre, Vincent David, Christophe Aussaguès, Guy Vidal-Naquet