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 |