Laboratoire Spécification et Vérification

The paper Constructive Completeness for the Linear-Time Mu-Calculus by Amina Doumane receives the Kleene Award for the Best Student Paper at LICS 2017 conference held in Reykjavik.

In celebration of two decades of activity, LSV is hosting a workshop to look back at achievements in our field and to discuss challenges ahead. The programme include invited talks by partners and members of the laboratory.

Members, former members, and other interested colleagues are cordially invited to join us in Cachan on 11 and 12 May. Attendance is free, but registration is required.

Semantics of Strategy Logic

Monday, 12 June 2017 at 2:00pm

Pavillon des Jardins, ENS Paris-Saclay

On the infinitary proof theory of logics with fixed points

Tuesday, 27 June 2017 at 10:00am

Université Paris-Diderot, Olympe-de-Gouges building, room 255

Professor Hubert Comon is 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.

Elie Bursztein, a former PhD student under Jean Goubault-Larrecq, and head of the anti-abuse research team at Google, Inc., Mountain View, CA, USA, has just publicized a major breach into the SHA1 cryptographic hash function, in common work between his team and Amsterdam's CWI. That attack was produced by using a combination of recent cryptoanalysis techniques run on CPU clusters and GPU clusters at Google, and allows one to produce counterfeit documents.

This attack has devastating consequences. SHA1 is used routinely to make Web sites secure, notably merchant sites (SSL/TLS), as well as email (PGP/GPG), backup systems, and is also used in everyday tools such as Git. Its estimated cost of only 110 000 USD makes it tractable.

For details of the attack, see the group's site: shattered.io.

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.

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

• Temporal logics on strings (PhD student)
• Decision procedures for separation logics (PhD student)
• VASS games for resource-bounded logics (PhD student)
• Effective concurrent infinite state systems (PhD student)
• Model Checking Well Structured Transition Systems (PhD student)
• Well Structured FIFO Automata (PhD student)