Logo IRISA      logo Inria

Le séminaire en bref

Le séminaire 68NQRT est un séminaire commun de l'IRISA et d'Inria Rennes. Il a lieu le jeudi à 14 heures par défaut dans la salle Markov. Les thèmes du séminaire recouvrent des thèmes étudiés dans les départements « réseaux, télécommunication et services » et « langage et génie logiciel » de l'IRISA, ou des thèmes « Algorithmique, programmation, logiciels et architectures » et  « Réseaux, systèmes et services, calcul distribué » d'Inria. On y trouve des exposés introductifs, avancés ou prospectifs dans les thèmes du génie logiciel, de l'informatique théorique, des mathématiques discrètes et de l'intelligence artificielle.

D'après Mathematical Subject Classification:
68 Computer Science
N Software
Q Theory of computing
R Discrete mathematics in relation to computer science
T Artificial intelligence

Prochain Exposé

jeudi 8 Décembre, 14h salle Aurigny

Alan Schmitt

Fully abstract encodings of lambda-calculus in HOcore through abstract machines

I will present fully abstract encodings of the call-by-name lambda-calculus into HOcore, a minimal higher-order process calculus which does not feature name restriction. We consider several equivalences on the lambda-calculus side—normal-form bisimilarity, applicative bisimilarity, and contextual equivalence—that we internalize into abstract machines in order to prove full abstraction.

Exposés des semaines suivantes

jeudi 15 Décembre, 14h salle Markov

Lucca Hirschi

Partial Order Reduction for Security Protocols.

Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g., anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools. In this paper, we overcome this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally eliminate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool Apte, and demonstrated that it achieves the expected speedup on various protocols.

jeudi 19 Janvier, 14h salle Markov

Romain Brenguier

To Be Announced

To Be Anounced

jeudi 26 janvier, 14h en salle Aurigny

Mahsa Shirmohammadi (To be confirmed)

To be Anounced

To Be Anounced

jeudi 9 mars, 14h

Pierre-Yves Strub (To be confirmed)

To be Anounced

To Be Anounced

jeudi 30 mars, 14h

Jérémie Chalopin

A counterexample to Thiagarajan's conjecture on regular event structures