« Return home

Publications

2007

R. Amadio A synchronous pi-calculus Information and Computation
R. Amadio, F. Dabrowski Feasible reactivity in a synchronous pi-calculus PPDP'07
G. Barthe, D. Pichardie, T. Rezk A certified lightweight non-interference Java bytecode verifier ESOP'07
G. Barthe, T. Rezk, A. Russo, A. Sabelfeld Security of multithreaded programs by compilation ESORICS'07
G. Boudol, M. Kolundzija Access control and declassification MMM-ACNS07
G. Boudol Fair cooperative multithreading CONCUR'07
I. Castellani State-oriented noninterference for CCS SecCo'07
S. Crafa, D. Varacca, N. Yoshida Event Structure Semantics for the Internal pi-calculus CONCUR'07
G. Le Guernic Automaton-based confidentiality monitoring of concurrent programs CSFS20
M. Huisman, C. Hurlin The stability problem for verification of concurrent object-oriented programs VAMP'07
M. Huisman and G. Petri The Java memory model: a formal explanation VAMP'07
D. Varacca, N. Yoshida Probabilistic pi-calculus and Event Structures QAPL'07

2008

R. Amadio, M. Dogguy Determinacy in a synchronous pi-calculus CUP
R. Amadio On convergence-sensitive bisimulation and the embedding of CCS in timed CCS EXPRESS 08
R. Amadio, M. Dogguy On affine usages in signal-based communication APLAS 08
G. Barthe, S. Cavadini, T. Rezk Tractable Enforcement of Declassification Policies CSF 08
F. Besson, G. Dufay, T. Jensen, D. Pichardie Verifying resource access control on mobile interactive devices JCS
G. Boudol Secure information flow as a safety property FAST'08
F. Boussinot, F. Dabrowski Safe reactive programming: the FunLoft proposal MULTIPROG
M. Dezani-Ciancaglini, S. Ghilezan, J. Pantovic, D. Varacca Security types for dynamic web data TCS
C. Fournet, T. Rezk Cryptographically sound implementations for typed information-flow POPL'08
C. Haack, C. Hurlin Separation logic contracts for a Java-like language with fork/join AMAST'08
C. Haack, C. Hurlin Resource usage protocols for iterators IWACO'08
C. Haack, M. Huisman, C. Hurlin Reasoning about Java's Reentrant Locks APLAS'08
A. Hobor, A. Appel, F. Zappa Nardelli Oracle semantics for concurrent separation logic ESOP'08
L. Hubert, T. Jensen, D. Pichardie Semantic Foundations and Inference of Non-null Annotations FMOODS'08
D. Pichardie Building certified static analysers by modular construction of well-founded lattices FICS 08

2009

J. Alglave, A. Fox, S. Isthiaq, M. Myreen, S. Sarkar, P. Sewell, F. Zappa Nardelli The semantics of Power and Arm multiprocessor machine code DAMP'09
R. Amadio On stratified regions APLAS'09
R. Amadio, P. Baillot, A. Madet An affine-intuitionistic system of types and effects: confluence and termination Tech. rep.
G.Barthe, B.Gregoire, C.Kunz, T.Rezk Certificate Translation for Optimizing Compilers TOPLAS
F. Besson, D. Cachera, T. Jensen, D. Pichardie Certified Static Analysis by Abstract Interpretation FOSAD'09
G. Boudol A Deadlock-Free Semnatics for Shared Memory Concurrency ICTAC'09
G. Boudol, G. Petri Relaxed Memory Models: an Operational Approach POPL'09
G. Castagna, L. Padovani Contracts for Mobile Processes CONCUR'09
F. Dabrowski, D. Pichardie A Certified Data Race Analysis for a Java-like Language TPHOLs'09
C.Fournet, G.Le Guernic,T.Rezk A Security-Preserving Compiler for Distributed Programs CCS
C. Hurlin Specifying and Checking Protocols of Multithreaded Classes SAC'09
S. Sarkar, P. Sewell, F. Zappa Nardelli, S. Owens, T. Ridge, T. Braibant, M. Myreen, J. Alglave The semantics of x86-CC multiprocessor machine code POPL'09
F. Zappa Nardelli, P. Sewell, J. Sevcik, S. Sarkar, S. Owens, L. Maranget, M. Batty, J. Alglave Relaxed Memory Models must be Rigorous EC^2'09

2010

J. Alglave, L. Maranget, P. Sewell, S. Sarkar Fences in Weak Memory Models CAV 10
G. Barthe, A. Hevia, Z. Luo, T. Rezk, B. Warinschi Robust Guarantees for Anonymity CSF 10
G. Boudol Typing termination in a higher-order concurrent imperative language Information and Computation 208
G.Boudol,Z.Luo, T.Rezk, M.Serrano Towards Reasoning for Web Applications: An Operational Semantics for Hop APLWACA
G. Boudol, G. Petri A theory of speculative computations ESOP 2010
S.Capecchi, I.Castellani, M.Dezani-Ciacaglini, T.Rezk Session Types for Access and Information Flow Control CONCUR
M. Dogguy, S. Glondu, S. Le Gall, S. Zacchiroli Enforcing type-safe linking using inter-package relationships JFLA'10
L. Hubert, T. Jensen, V. Monfort, D. Pichardie. Enforcing secure object initialization in Java ESORICS 2010
T. Wrigstad, F. Zappa Nardelli, S. Lebresne, J. Ostlund, J. Vitek Integrating Typed and Untyped Code in a Scripting Language POPL'10

2011

J. Sevcik, V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, P. Sewell Relaxed-Memory Concurrency and Verified Compilation POPL'11