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.


PhD Defense: Pierre Halmagrand

Visit website for this news | Export event in iCalendar format

PhD Pierre Halmagrand

Automated Deduction and Proof Certification for the B Method
Saturday, 10 December 2016 at 2pm
CNAM, Amphithéâtre Abbé-Grégoire
292 rue Saint-Martin, 75003 Paris

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.

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.

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.

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

S. Delaune and L. HirschiA survey of symbolic methods for establishing equivalence-based properties in cryptographic protocolsJournal of Logic and Algebraic Methods in Programming, 2016. To appear. Web page | PDF | BibTeX )
P. Beame, N. Grosshans, P. McKenzie and L. SegoufinNondeterminism and an abstract formulation of Neciporuk's lower bound method.  Research Report 1608.01932, Computing Research Repository, August 2016. 34 pages. PDF | BibTeX )
F. Bruse, N. Kobayashi and É. LozesOn the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint LogicIn POPL'17. ACM Press, January 2017. To appear. 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

Sat, Dec 10
Tue, Jan 17


Antoine Dallon and Jérémie Dubut receive ED STIC Award

Antoine Dallon and Jérémie Dubut receive the First Price for the Best Scientific Contribution awarded by the STIC Doctoral School of Université Paris-Saclay. The award ceremony was held during the ED STIC PhD Days on Wednesday 16 November at ENSTA ParisTech.

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.