Parallelism and Security
Program
| 10h-10h30 | meeting | ||
| 10h30-11h10 | D. Varacca | Parallel extrusion in the pi-calculus | |
| 11h10-11h50 | G. Petri | TBA | |
| 11h50-12h30 | M. Dogguy | TBA | |
| 12h30-14h | lunch | ||
| 14h-14h40 | D. Pichardie | Secure the Clones | |
| 14h40-15h20 | K. Bhargavan | Type-checking higher-order security libraries | |
| 15h20-15h40 | pause | ||
| 15h40-16h20 | F. Zappa Nardelli | Relaxed memory concurrency and verified compilation | |
| 16h20-17h | Panel | what's next? |
Participants
G. Petri, F. Zappa Nardelli, I. Castellani, T. Rezk, G. Boudol, T. Jensen, M. Dogguy, D. Varacca, D. Pichardie.
Program
| 10h30-11h | meeting | ||
| 11h-11h45 | A. Madet | An affine-intuitionistic system of types and effect: confluence and termination | |
| 11h45-12h30 | T. Rezk | Code injection | |
| 12h30-14h | discussion and lunch | ||
| 14h-14h45 | G. Boudol | A type system to guarantee sequential consistency in RMO + barriers | |
| 14h45-15h30 | P. Pawan | A daemonic x86-TSO emulator | |
| 15h30-16h | discussion and pause | ||
| 16h-16h45 | N. Guts | Type inference for F7 | |
| 16h45-17h30 | I. Castellani | Session types for access and information flow control |
Participants
A. Madet, G. Petri, F. Zappa Nardelli, J.J. Lévy, I. Castellani, T. Rezk, G. Boudol, T. Jensen, M. Dogguy, N. Guts, F. Dabrowski, B. Serpette, P. Pawan, Z. Luo, P. Attar, J. Grand, T. Gazagnaire.
Program
| 10h15-10h40 | meeting | ||
| 10h40-11h20 | D. Pichardie | Secure Cloning | |
| 11h20-12h00 | G. Petri | A theory of speculative computations | |
| 12h-13h30 | discussion and lunch | ||
| 13h30-14h10 | G. Manzonetto | Resource calculi: some syntax, some semantics | |
| 14h10-14h50 | G. Castagna | Contracts for Mobile Processes | |
| 14h50-15h20 | discussion and pause | ||
| 15h20-16h00 | T. Rezk | Security in Hop web applications | |
| 16h00-16h40 | G. Le Guernic | Cryptographically Secured Information Flows of Distributed Programs |
Participants
G. Castagna, G. Petri, F. Zappa Nardelli, J.J. Lévy, I. Castellani, T. Rezk, G. Boudol, T. Jensen, R. Amadio, G. Manzonetto, M. Dogguy, J. Planul, N. Guts, D. Pichardie, G. Le Guernic, A. Bucciarelli
Program
| 10h-11h | F. Zappa Nardelli | Like Types | |
| 11h-12h | J. Alglave | The Power memory model | |
| 12h-13h30 | discussion and lunch | ||
| 13h30-14h15 | G. Boudol | A semantics without deadlocks | |
| 14h15-15h | B. Serpette | Qui sème la fonction récolte le tuyau typé | |
| 15h-15h30 | discussion and pause | ||
| 15h30-16h15 | F. Dabrowski | Iteration sensitive escape analysis | |
| 16h15-17h00 | R. Amadio | Termination of lambda-calculus with references |
Participants
F. Boussinot, G. Petri, F. Zappa Nardelli, J.J. Lévy, F. Dabrowski, I. Castellani, T. Rezk, G. Boudol, T. Jensen, J. Alglave, L. Maranget, B. Serpette
Program
| 11h30-12h | C. Hurlin | Automatic parallelization based on proof rewriting | |
| 12h-12h30 | F. Boussinot | The ANR PARTOUT project | |
| 12h30-14h30 | discussion and lunch | ||
| 14h30-15h | T. Rezk | A compiler for security | |
| 15h-15h30 | R. Amadio | On convergence sensitive bisimulation | |
| 15h30-16h | F. Dabrowski | Towards a formal semantics of MIDP graphical user interfaces | |
| 16h-16h30 | discussion and pause | ||
| 16h30-17h00 | D. Pichardie | A certified data race analysis for a Java-like language | |
| 17h00-17h30 | C. Hurlin | Size does matter |
Participants
F. Boussinot, G. Petri, F. Zappa Nardelli, J.J. Lévy, D. Pichardie, F. Dabrowski, I. Castellani, C. Hurlin, T. Rezk, G. Boudol, T. Jensen, L. Maranget
Program
| 11h-1130h | F. Zappa Nardelli | The Intel 64/ia-32 relaxed memory model | |
| 11h30-12h | D. Varacca | The meaning of causal labelled bisimulations | |
| 12h-12h30 | G. Boudol | Secure information flow as a safety property | |
| 12h30-14h30 | discussion and lunch | ||
| 14h30-15h | G. Pietri | On relaxed memory models | |
| 15h-15h30 | F. Dabrowski | Formalisation of static analysis for multithreaded Java | |
| 15h30-16h | J. Vitek | Flexible Task Graphs | |
| 16h-16h30 | discussion and pause | ||
| 16h30-17h00 | C. Hurlin | Separation logic for a Java-like language | |
| 17h00-17h30 | F. Zappa Nardelli | Oracle Semantics for Concurrent Cminor (.pptx) |
Participants
G. Pietri, G. Boudol, C. Hurlin, I. Castellani, F. Boussinot, F. Dabrowski, D. Pichardie, T. Jensen, R. Amadio, M. Dogguy, D. Varacca, J. Vitek, F. Zappa Nardelli.
Program
| 10h-11h | F. Zappa Nardelli | Ott: effective tool support for the working semanticist |
| 11h-12h | G. Barthe | Certificate translation for optimizing compilers |
| 12h-13h | F. Dabrowski | Data races in Java and static analysis |
| 13h-14h | lunch | |
| 14h-15h | G. Boudol | Typing termination in a higher-order, concurrent, imperative language |
| 15h-16h | G. Castagna | A theory of contracts for web services |
| 16h-17h | M. Dogguy | Linear usages in signal-based communication |
Participants
F. Boussinot, G. Le Guernic, F. Dabrowski, D. Pichardie, G. Castagna, D. Kesner, R. Di Cosmo, G. Barthe, O. Danvy, E. Giacchino, R. Amadio, M. Dogguy, F. Zappa Nardelli, G. Boudol, I. Castellani, M. Kolundzija, C. Hurlin, J-J. Lévy, D. Varacca.
Program
| 10h-10h30 | breakfast | ParSec organisation |
| 10h30-11h | A. Appel | Threads can be implemented as a (semantic) library |
| 11h-11h30 | J. Alglave | Certified symbolic execution with separation logic. |
| 11h30-12h | C. Hurlin | Permission based verification of dara race freeness for lock free programs |
| 12h-13h30 | lunch | |
| 13h30-14h | I. Castellani | State-oriented noninterference for CCS |
| 14h-14h30 | D. Varacca | Event structure semantics for untyped pi-calculus. |
| 14h30-15h | R. Amadio | Determinacy in a synchronous pi-calculus |
| 15h-15h30 | pause | |
| 15h30-16h | C. Fournet | Secure implementations for Typed Session Abstractions |
| 16h-16h30 | G. Le Guernic | Automaton-based Confidentiality Monitoring of Concurrent Programs. |
| 16h30-17h | M. Kolundzija | Acces control and declassification. |
Participants
J. Alglave, F. Boussinot, G. Le Guernic, F. Dabrowski, A. Appel, D. Pichardie, T. Rezk, C. Fournet, R. Amadio, M. Dogguy, F. Zappa Nardelli, O. Tardieu, G. Boudol, I. Castellani, M. Kolundzija, M. Huisman, C. Hurlin, J-J. Lévy, D. Varacca.
Program
| 9h30-10h30 | G. Boudol | Research on Security in the Mimosa research team |
| 10h30-11h | pause | |
| 11h-12h | G. Barthe | Les travaux dans l'équipe Everest |
| 12h-12h30 | J-J. Lévy | History based flow analysis |
| 12h30-14h | déjeuner | |
| 14h-14h45 | D. Pichardie | A certified static analyser in constructive logic |
| 14h45-15h15 | F. Besson | Language-based access control |
| 15h15-16h | R. Amadio | A synchronous pi-calculus |
| 16h-16h15 | pause | |
| 16h15-17h | F. Zappa Nardelli | Concurrent CMinor |
| 17h-17h30 | D. Varacca | Déterminisme et structures d'événements dans le pi-calcul |
Participants
R. Amadio, G. Barthe, F. Besson, G. Boudol, F. Boussinot, S. Cavadini, I. Castellani, F. Dabrowski, M. Huisman, C. Hurlin, T. Jensen, M. Kolundzija, J-J. Lévy, G. Petri, D. Pichardie, T. Rezk, O. Tardieu, D. Varacca, F. Zappa Nardelli.