Depuis le 1er janvier 2021, le LSV forme avec l'équipe Vals du LRI le "Laboratoire Méthodes Formelles". Le LMF est une unité mixte de recherche (UMR9021) entre l'Université Paris-Saclay, le CNRS et l'ENS Paris-Saclay. Le LMF a deux partenaires, CentraleSupélec et Inria. Le site web du nouveau laboratoire se trouve ici :
https://lmf.cnrs.fr


Laboratoire Spécification et Vérification

Fondé en 1997, le Laboratoire Spécification et Vérification (LSV) est le laboratoire d'informatique de l'ENS Paris-Saclay, et est aussi affilié au Centre National de la Recherche Scientifique (CNRS) en tant qu'UMR 8643. La recherche au LSV est centrée sur la vérification de logiciels et systèmes critiques, et sur la vérification de la sécurité des systèmes informatiques.

À la une

Motion du futur Laboratoire Méthodes Formelles contre la LP(P)R

Le projet de loi LP(P)R est présenté à partir du 21 septembre à l'Assemblée Nationale, puis fin octobre au Sénat, en procédure accélérée. Malgré une mobilisation sans précédent des agents de l'enseignement supérieur et la recherche, la proposition de loi persiste dans une politique ne permettant pas d'avoir une vision à long terme pour une recherche fondamentale : renforcement du financement par des projets à court terme via l'ANR, précarisation des emplois (CDI de chantier et tenure track), ... Indépendemment des ces deux points majeurs, les fonds promis permettront à peine d'atteindre 0,85% du PIB en 2030 pour la recherche publique, contrairement à l'engagement de l'ensemble des pays de l'UE (engagement qui est rappelé dans les objectifs de la LP(P)R) de le porter à 1% du PIB.

En parallèle, le ministère essaie de faire signer aux syndicats, dans l'urgence, un protocole d'accord qui ne garantit rien mais est sous contrainte de ratifier la LP(P)R.

Le calendrier et la manière de présenter cette loi a tout du passage en force : présentation devant le CNESER avec un vote à 6h45 du matin, procédure accélérée devant les chambres, protocole d'accord proposé moins d'un mois avant la présentation à l'assemblée, ... Tout cela dans une période extrêmement difficile pour les chercheur∑se∑s et enseignant∑e∑s-chercheur∑se∑s.

Nous, le Laboratoire de Méthodes Formelles, refusons toujours une loi qui va renforcer la précarité, la recherche à court terme, la concurrence malsaine et individuelle entre chercheur∑se∑s. Nous soutenons les actions de mobilisation de la communauté et demandons une nouvelle fois le retrait de la LP(P)R.

28 septembre 2020

Actualités

CONCUR 2020 Best-Paper Award

Visit website for this news

CONCUR Award

Benedikt Bollig, Alain Finkel, and Amrita Suresh ont reçu le Best-Paper Award à CONCUR 2020 pour leur article Bounded Reachability Problems are Decidable in FIFO Machines. Un deuxième article co-écrit par nos collègues a fait partie des 4 nominations: Patricia Bouyer, Stephane Le Roux, Youssouf Oualhadj, Mickael Randour and Pierre Vandenhove, Games Where You Can Play Optimally with Arena-Independent Finite Memory.

Un nouveau modèle pour les rèeaux biologiques

Visit website for this news

Dans un nouvel article publié dans Nature Communications, nos collegues Juraj Kolĉàk, Thomas Chatain et Stefan Haar, avec Loïc Paulevé du LaBRI, proposent une méthode efficace de modélisation des réseaux biologiques à l'échelle du génome qui échappe aux limites des réseaux booléens utilisés aujourd'hui. L'avancée est présenté dans les Actualitès de CNRS-INS2I par Loïc Paulevé et de Inria par Stefan Haar.

Le COVID-19 menace aussi nos vies privées

L'informatique fait partie des moyens à notre disposition pour lutter contre la pandémie de COVID-19. Attestations de non-contamination, contrÙle des conditions de quarantaine ou de confinement, prédiction des infections par "contact tracing"... En savoir plus

Entretien avec Alain Finkel, membre senior de l'IUF

Visiter le site web pour cet événement

Alain Finkel nominated at Institut Universitaire de France

Alain Finkel a ètè nommé à l'Institut universitaire de France en tant que membre senior. L'INS2I du CNRS vient du publier un entretien avec Alain sur ses nouveaux projets.

PhD Defense : Alessio Mansutti

Alessio

Reasoning with Separation Logic: Complexity, Expressive Power, Proof Systems
Thursday, 10 December 2020 at 3:30pm
ENS Paris-Saclay/Online

Soutenance : Marie Fortin

Marie Fortin

Expressivity of first-order logic, star-free propositional dynamic logic and communicating automata
Friday, 27 novembre 2020 à 10h30am
ENS Paris-Saclay/Online

À propos du LSV

    

Contacter le LSV

Exporter l'adresse au format vCard | Informations d'accès

photo LSV
Adresse
LSV, CNRS & ENS Paris-Saclay
4 avenue des Sciences
91190 Gif-sur-Yvette, France

Informations d'accès

Liens directs

Distinctions

CSF 2020 Distinguished Paper Award

Visit website for this news

Solène Moreau a reçu le Distinguished-Paper Award à CSF 2020.

Prix doctorands EDSTIC 2019

Visit website for this news

Deux doctorands du LSV ont été laureats du prix de thèe de l'ecole doctorale STIC 2019 : Adrien Koutsos, 5G-AKA Authentication Protocol Privacy -- premier prix ex-aequo, Marie Fortin, FO = FO3 for Linear Orders with Monotone Binary Relations -- deuxème prix ex-aequo.


Jean-Christophe Filliâtre reçoit le CAV Award 2019

Visit website for this news

Le prix CAV Award 2019 est atribué à Jean-Christophe Filliâtre, membre de l'equipe VALS du LRI et futur collègue au sein du laboratoire Méthodes Formelles, pour ses travaux sur les langages de vérification intermédiaires réutilisables qui ont considérablement simplifié et accéléré la construction de vérificateurs déductifs automatisés.

Le prix récompense annuellement des contributions fondamentales au domaine de la vérification assistée par ordinateur. En 2017, le CAV Award a été décerné à nos collègues Alain Finkel et Philippe Schnoebelen.