Laboratoire Spécification et Vérification

Founded in 1997, the Laboratoire Spécification et Vérification (LSV) is the Computer Science laboratory of ENS de Cachan, and is also affiliated to the French Centre National de la Recherche Scientifique (CNRS) as UMR 8643. Research at LSV is focused on the verification of critical software and systems, as well as on the verification of computer system security.


Statement on the Secure Electronic Documents database TES

Visit website for this news

Le Laboratoire Spécification et Vérification (LSV), laboratoire d'informatique de l'ENS Paris-Saclay et du CNRS affirme que l'instauration du nouveau fichier "titres électroniques sécurisés" prévue par le décret №2016-1460, comporte un risque inhérent majeur d'attaque, vol et détournement à l'heure où les attaquants informatiques disposent de moyens considérables et croissants. Le LSV ne connaît pas de solution technique centralisée permettant de réaliser toutes les fonctionnalités prévues par le décret tout en garantissant la confidentialité des données des citoyens.

Next Seminar

A Model Checking Approach to Dynamical Systems Analysis

Visit website for this news | Export event in iCalendar format

SEM David  Safranek
Tuesday, January 24 2017 at 11:00AM
Salle de Conférence (Pavillon des Jardins)
David Safranek (Masaryk University, Brno)


Hubert Comon at Institut Universitaire de France

Visit website for this news

Hubert Comon at Institut Universitaire de France

Professor Hubert Comon has been named Senior Member of the Institut Universitaire de France. During his five-year membership term, he will pursue a project on Computer Security and Formal Methods.

Open Positions

See the job openings

There are several open positions for students interested in the research topics investigated at LSV, including the following funded PhD and postdoc openings:

Recent publications

Visit the corresponding web page Register to the RSS feed of LSV publications

P. Beame, N. Grosshans, P. McKenzie and L. SegoufinNondeterminism and An Abstract Formulation of Neciporuk's Lower Bound MethodACM Transactions on Computation Theory 9(1), pages 5:1-5:34, 2016. BibTeX )
E. André, Th. Chatain and C. RodríguezPreserving Partial-Order Runs in Parametric Time Petri NetsACM Transactions in Embedded Computing Systems 16(2), pages 43:1-43:26, 2017. PDF | BibTeX )
P. Bouyer and V. JugéDynamic Complexity of the Dyck ReachabilityIn FoSSaCS'17, LNCS. Springer, April 2017. Web page | BibTeX )

About LSV

LSV Contact Information

Export in vCard format | Access information

LSV photo
LSV, CNRS & ENS de Cachan
61, avenue du Président Wilson
94235 CACHAN Cedex, France
+33 1 47 40 75 20
+33 1 47 40 75 21

Access information


Export agenda in iCalendar format | LSV seminars page

Tue, Jan 24
Tue, Feb 21


EATCS Distinguished Dissertation Award 2016

Visit website for this news

EATCS Distinguished Dissertation Award 2016

Georg Zetzsche received the Distinguished Dissertation Award 2016 of the EATCS for his thesis Monoids as storage mechanisms at the University of Kaiserslautern, Germany. Georg Zetzsche is currently a post-doc at LSV in the INFINI axis.

EASST Best Paper Award at ETAPS 2016

EASST Best Paper Award at ETAPS 2016

Véronique Cortier, Antoine Dallon, and Stéphanie Delaune received the EASST Best Paper Award at ETAPS 2016 for their paper Bounding the number of agents, for equivalence too presented at POST 2016.

Stéphanie Delaune awarded ERC Starting Grant

Visit website for this news

Stéphanie Delaune  
 awarded ERC Starting Grant

Stéphanie Delaune received an ERC Starting Grant for her project POPSTAR - Physical properties Of security Protocols with an Application To contactless Systems. The objective of the project is to develop foundations and practical tools to analyse the security and privacy of modern security protocols that establish and rely on physical properties.

Stéphanie is a CNRS-Researcher, she has been a member of LSV since 2007 before joining the EMSEC team at IRISA, Rennes in September 2016.