@INPROCEEDINGS{HuismanH07b,
author = {Marieke Huisman and Cl\'ement Hurlin},
title = {Permission Specifications for Common Multithreaded Programming Patterns},
booktitle = {Reflections
on Type Theory, Lambda Calculus, and the Mind. Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday},
year = 2007,
topics = {team},
pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/patterns.pdf}
}
@INPROCEEDINGS{GurovHS08,
author = {D. Gurov and M. Huisman and C. Sprenger},
title = {An Algorithmic Approach to Compositional Verification of Sequential Programs with Procedures: An Overview},
booktitle = {Foundations of Interface Technologies (FIT 2008)},
year = 2008,
editors = {K.G. Larsen and A. Wasowski and U. Nyman},
topics = {team},
pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/fit.pdf}
}
@ARTICLE{GregoireS07,
author = {Benjamin Gr{\'e}goire and Jorge Luis Sacchini},
title = {Combining a Verification Condition Generator for a Bytecode
Language with Static Analyses},
year = {2007},
note = {To appear},
topics = {team}
}
@ARTICLE{ZanellaWMM07,
author = {Gilles Barthe and Bejamin Gr{\'e}goire and
Romain Janvier and Santiago Zanella B{\'e}guelin},
title = {A Framework for Language-Based Cryptographic Proofs},
booktitle = {2nd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory},
month = {Oct},
year = {2007},
topics = {team}
}
@INPROCEEDINGS{HurlinCFMW07,
author = {Cl\'ement Hurlin and Amine Chaieb and Pascal Fontaine and Stephan Merz and Tjark Weber},
title = {Practical Proof Reconstruction for First-Order Logic and Set-Theoretical Constructions},
booktitle = {\href{http://homepages.inf.ed.ac.uk/ldixon/events/isabelle-ws-07/}{Isabelle Workshop (ISABELLE-WS)}},
editor = {Lucas Dixon and Moa Johansson},
pages = {2--13},
year = {2007},
address = {Bremen, Germany},
pdfurl = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/isabellews07.pdf},
texurl = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/isabellews07.tex},
topics = {team}
}
@INPROCEEDINGS{Zanella:2005:CASSIS,
author = {S. {Zanella B{\'e}guelin}},
title = {Formalisation and Verification of the {GlobalPlatform
Card Specification} Using the {B} Method},
booktitle = {Construction and Analysis of Safe, Secure, and Interoperable
Smart Devices, Second International Workshop, CASSIS 2005,
Nice, France, March 8--11 2005},
editor = {G. Barthe and B. Gr{\'e}goire and M. Huisman and J.-L. Lanet},
volume = {3956},
series = {Lecture Notes in Computer Science},
year = {2005},
pages = {155--173},
publisher = {Springer-Verlag},
isbn = {3-540-33689-3},
url = {http://dx.doi.org/10.1007/11741060_9},
topics = {team}
}
@MISC{gdt06:hal,
author = {G. Barthe and D. Naumann and T. Rezk},
title = {Deriving an Information Flow Checker and Certifying Compiler for {Java}},
year = {2006},
note = {To appear},
topics = {team}
}
@TECHREPORT{gdt06:jvm,
author = {G. Barthe and D. Pichardie and T. Rezk},
title = {Deriving an Information Flow Checker for the {JVM}},
year = {2006},
topics = {team},
institution = {INRIA}
}
@INPROCEEDINGS{GT:ijcar06,
author = {B. Gr\'egoire and L. Thery},
title = {A purely functional library for modular arithmetic and its application for certifying large prime numbers},
topics = {team},
pages = {423-437},
booktitle = {Proceedings of IJCAR'06},
year = 2006,
publisher = {Springer-Verlag},
series = {Lecture Notes in Artificial Intelligence},
volume = 4130,
editor = {U. Furbach and N. Shankar},
pdfurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/numlib.pdf}
}
@INPROCEEDINGS{GH05,
author = {D. Gurov and M. Huisman},
title = {Interface Abstraction for Compositional Verification},
crossref = {sefm05},
pages = {414-423},
psurl = {http://www.nada.kth.se/~dilian/Papers/sefm05.ps.gz},
note = {An earlier version appeared as INRIA Technical Report, nr. RR-5330},
topics = {team}
}
@TECHREPORT{gpt06:hal,
author = {G. Barthe and P. D'Argenio and T. Rezk},
title = {{Secure Information Flow by Self-Composition}},
topics = {team},
year = {2006},
institution = {INRIA}
}
@ARTICLE{g+:jakarta,
author = {G. Barthe and P. Courtieu and G. Dufay and S. Melo de
Sousa},
title = {{Jakarta: tool-assisted specification and verification of
the JavaCard Platform}},
year = {200x},
journal = {{Journal of Automated Reasoning}},
note = {To appear},
topics = {team,castles}
}
@PHDTHESIS{Bar:hdr,
title = {De la th\'eorie des types \`a la v\'erification formelles
des petits objets portables de s\'ecurit\'e},
author = {G. Barthe},
year = {2004},
school = {Universit\'e de Nice Sophia-Antipolis},
type = {Habilitation {\`a} Diriger des Recherches},
topics = {team}
}
@PHDTHESIS{JLL:hdr,
title = {Produire des logiciels s\^urs},
author = {J.-L. Lanet},
year = {2004},
school = {Universit\'e de Marseille},
type = {Habilitation {\`a} Diriger des Recherches},
topics = {team}
}
@PHDTHESIS{Catano:phd,
title = {Formal methods for Java Programs},
author = {N. Cata{\~n}o},
year = {2004},
school = {Universit\'e de Paris},
topics = {team}
}
@PHDTHESIS{Rezk:phd,
title = {Verification of confidentiality policies for mobile code},
author = {T. Rezk},
year = {2006},
school = {Universit\'e de Nice Sophia-Antipolis},
topics = {team}
}
@PHDTHESIS{Pavlova:phd,
title = {Specification and verification of Java bytecode},
author = {M. Pavlova},
year = {2007},
school = {Universit\'e de Nice Sophia-Antipolis},
topics = {team}
}
@PHDTHESIS{Tarento:phd,
title = {Formalisation en Coq de modeles cryptographiques et application au cryptosysteme ElGamal},
author = {S. Tarento},
year = {2006},
school = {Universit\'e de Nice Sophia-Antipolis},
topics = {team}
}
@PHDTHESIS{SouPhd,
author = {S. Melo de Sousa},
title = {Outils et techniques pour la v\'erification formelle de la plate-forme JavaCard},
school = {INRIA/Universidade de Nice-Sophia Antipolis},
year = {2003},
month = {February},
psurl = {http://www.di.ubi.pt/~desousa/tese.ps},
topics = { team,castles }
}
@TECHREPORT{BGHKJ-5331,
author = {F. Bellegarde and J. Groslambert and M. Huisman and O. Kouchnarenko and J. Julliand},
title = {Verification of Liveness Properties with {JML}},
institution = {INRIA},
year = {2004},
number = {RR-5331},
topics = {team},
psurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/liveness.ps.gz}
}
@INPROCEEDINGS{DBLP:conf/cardis/CourbotPGV06,
author = {A. Courbot and
M. Pavlova and
G. Grimaud and
J.J. Vandewalle},
title = {A Low-Footprint {Java}-to-Native Compilation Scheme Using
Formal Methods.},
booktitle = {proceedings of CARDIS},
year = {2006},
pages = {329-344},
ee = {http://dx.doi.org/10.1007/11733447_24},
crossref = {DBLP:conf/cardis/2006},
bibsource = {DBLP, http://dblp.uni-trier.de},
topics = {team}
}
@TECHREPORT{GurovHS06,
author = {D. Gurov and M. Huisman and C. Sprenger},
title = {Compositional Verification of Sequential Programs with Procedures},
institution = {INRIA},
year = {2006},
topics = {team}
}
@INPROCEEDINGS{BARTHE-EA-tgc06,
author = {Gilles~Barthe
and Lennart~Beringer
and Pierre~Cr\'egut
and Benjamin~Gr\'egoire
and Martin~Hofmann
and Peter~M{\"u}ller
and Erik~Poll
and Germ\'{a}n~Puebla
and Ian~Stark
and Eric~V\'etillard},
title = {MOBIUS: Mobility, Ubiquity, Security. Objectives and progress
report},
booktitle = {TGC 2006: Proceedings of the second symposium on Trustworthy
Global Computing},
series = {LNCS},
publisher = {Springer-Verlag},
year = {2006},
topics = {team},
url = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/tgc06.pdf}
}
@PROCEEDINGS{flops06,
booktitle = {Proceedings of FLOPS'06},
title = {Proceedings of FLOPS'06},
year = 2006,
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 3945,
editor = {M. Hagiya and P. Wadler}
}
@PROCEEDINGS{sp06,
booktitle = {Proceedings of Symposium of Security and Privacy'06},
title = {Proceedings of Proceedings of Symposium of Security and Privacy '06},
year = 2006,
publisher = {IEEE Press},
editor = {}
}
@PROCEEDINGS{sefm05,
title = {Software Engineering and Formal Methods (SEFM'05)},
booktitle = {Proceedings of SEFM'05},
editor = {B. Aichernig and B. Beckert},
publisher = {IEEE Computer Society},
month = {September},
address = {Koblenz, Germany},
year = 2005
}
@PROCEEDINGS{fosad05,
year = {2005},
booktitle = {Proceedings of FOSAD'05},
editor = {A.~Aldini and R.~Gorrieri and F.~Martinelli},
series = {Lecture Notes in Computer Science},
volume = {3655},
publisher = {Springer-Verlag}
}
@PROCEEDINGS{fast05,
booktitle = {Proceedings of FAST'05},
year = 2005,
editor = {R.~Gorrieri and F.~Martinelli and P.~Ryan and S.~Schneider},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {3866}
}
@PROCEEDINGS{esorics05,
title = {Proceedings of {ESORICS}'05},
booktitle = {Proceedings of {ESORICS}'05},
year = {2005},
editor = {S. De Capitani di Vimercati and P.F. Syverson and D. Gollmann},
volume = {3679},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
@PROCEEDINGS{cats05,
title = {Proceedings of CATS'05},
booktitle = {Proceedings of CATS'05},
year = 2005,
editor = {M. Atkinson and F. Dehne},
volume = 41,
series = {Conferences in Research and Practice in Information Technology},
address = {Newcastle, Australia},
month = {February},
publisher = {ACSC}
}
@PROCEEDINGS{qapl05,
title = {Proceedings of 3rd Workshop on Quantitative Aspects of
Programming Languages (QAPL'05)},
booktitle = {Proceedings of 3rd Workshop on Quantitative Aspects of
Programming Languages (QAPL'05)},
year = {2005},
address = {Edinburgh, Scotland },
publisher = {Electronic Notes in Theoretical Computer Science},
note = {to appear}
}
@PROCEEDINGS{tlca05,
title = {Proceedings of {TLCA}'05},
booktitle = {Proceedings of {TLCA}'05},
year = {2005},
editor = {P. Urzyczyn},
volume = 3641,
series = {Lecture Notes in Computer Science},
address = {Nara, Japan},
month = {April},
publisher = {Springer-Verlag}
}
@PROCEEDINGS{csl05,
title = {Proceedings of CSL'05},
booktitle = {Proceedings of CSL'05},
year = {2005},
address = {Oxford, UK},
month = {August},
volume = {3634},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
editor = {L. Ong}
}
@PROCEEDINGS{tphol05,
title = {Proceedings of TPHOLs'05},
booktitle = {Proceedings of TPHOLs'05},
editor = {J. Hurd and T. Melham},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 3603,
year = {2005},
address = {Oxford, UK},
month = {August}
}
@PROCEEDINGS{tldi05,
title = {Proceedings of {TLDI}'05},
booktitle = {Proceedings of {TLDI}'05},
year = {2005},
editor = {M. F\"ahndrich},
publisher = {ACM Press},
month = {January},
address = {Long Beach, USA}
}
@PROCEEDINGS{types04,
year = {2005},
editor = {J.C. Filli\^atre and C. Paulin-Mohring and B. Werner},
booktitle = {Proceedings of {TYPES}'04},
title = {Proceedings of {TYPES}'04},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {3839}
}
@PROCEEDINGS{csfw04,
title = {Proceedings of CSFW'04},
booktitle = {Proceedings of CSFW'04},
year = {2004},
editor = {R. Foccardi},
publisher = {IEEE Press},
address = {Pacific Grove,USA},
month = {June}
}
@PROCEEDINGS{ijcar04,
year = {2004},
title = {Proceedings of IJCAR'04},
booktitle = {Proceedings of IJCAR'04},
editor = {D. Basin and M. Rusinowitch},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {3097},
address = {Cork, Ireland},
month = {July}
}
@PROCEEDINGS{cardis04,
editor = {P. Paradinas and J.-J. Quisquater},
booktitle = {{Proceedings of CARDIS'04}},
title = {{Proceedings of CARDIS'04}},
publisher = {Kluwer Academic Publishers},
year = {2004},
address = {Toulouse, France},
month = {August}
}
@PROCEEDINGS{fmse04,
booktitle = {Proceedings of FMSE'04},
title = {Proceedings of FMSE'04},
editor = {M. Backes and D. Basin and M. Waidner},
publisher = {ACM Press},
year = 2004,
address = {Washington D.C., USA},
month = {October}
}
@PROCEEDINGS{memocode04proc,
booktitle = {Memocode'04},
title = {Memocode'04},
year = {2004},
publisher = {IEEE Computer Society},
editor = {C. Heitmeyer and J.-P. Talpin}
}
@PROCEEDINGS{fase04,
year = {2004},
booktitle = {Proceedings of {FASE}'04},
title = {Proceedings of {FASE}'04},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {2984},
editor = {M. Wermelinger and T. Margaria-Steffen},
address = {Barcelona, Spain},
month = {March}
}
@PROCEEDINGS{vmcai04,
year = {2004},
booktitle = {Proceedings of {VMCAI}'04},
title = {Proceedings of {VMCAI}'04},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {2934},
editor = {B. Steffen and G. Levi},
address = {Venice, Italy},
month = {January}
}
@PROCEEDINGS{vmcai03,
booktitle = {VMCAI: Verification, Model Checking and Abstract Interpretation},
title = {VMCAI: Verification, Model Checking and Abstract Interpretation},
editor = {L. D. Zuck and P. C. Attie and A. Cortesi and S. Mukhopadhyay},
volume = {2575},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
month = {January 9-11},
year = {2003}
}
@PROCEEDINGS{fmics03,
booktitle = {FMICS: Eighth International Workshop on Formal Methods for Industrial Critical Systems},
title = {FMICS: Eighth International Workshop on Formal Methods for Industrial Critical Systems},
editor = {T. Arts and W. Fokkink},
volume = {80},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Publishing},
month = {June 5-7},
year = {2003}
}
@PROCEEDINGS{rta03,
year = {2003},
booktitle = {Proceedings of RTA'03},
title = {Proceedings of RTA'03},
editor = {R. Nieuwenhuis},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {2706},
address = {Valencia, Spain},
month = {June}
}
@PROCEEDINGS{popl03,
booktitle = {Proceedings of POPL'03},
title = {Proceedings of POPL'03},
year = {2003},
publisher = {ACM Press},
address = {New Orleans, USA},
month = {January}
}
@PROCEEDINGS{zb03,
booktitle = {ZB 2003: Formal Specification and Development in Z and B},
title = {ZB 2003: Formal Specification and Development in Z and B},
volume = {2651},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
year = {2003},
editor = {D. Bert and J.P. Bowen and S. King and M. Wald\'en}
}
@PROCEEDINGS{fme03,
booktitle = {FME 2003: Formal Methods: International Symposium of Formal Methods Europe},
title = {FME 2003: Formal Methods: International Symposium of Formal Methods Europe},
editor = {K. Araki and S. Gnesi and D. Mandrioli},
volume = {2805},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
year = {2003}
}
@PROCEEDINGS{fase02,
booktitle = {Fundamental Approaches to Software Engineering (FASE'02)},
title = {Fundamental Approaches to Software Engineering (FASE'02)},
year = {2002},
series = {Lecture Notes in Computer Science},
volume = {2306},
publisher = {Springer-Verlag}
}
@PROCEEDINGS{fme02,
booktitle = {FME 2002: Formal Methods: International Symposium of Formal Methods Europe},
title = {FME 2002: Formal Methods: International Symposium of Formal Methods Europe},
year = {2002},
editor = {L.-H. Eriksson and P. Lindsay},
volume = {2391},
series = {Lecture Notes in Computer Science},
address = {Copenhagen, Denmark},
month = {July},
publisher = {Springer-Verlag}
}
@PROCEEDINGS{amast02,
booktitle = {Proceedings of AMAST'02},
title = {Proceedings of AMAST'02},
editor = {H. Kirchner and C. Ringessein},
series = {Lecture Notes in Computer Science},
year = {2002},
publisher = {Springer-Verlag},
volume = {2422}
}
@PROCEEDINGS{DBLP:conf/cardis/2006,
editor = {J. Domingo-Ferrer and
J. Posegga and
D. Schreckling},
title = {Smart Card Research and Advanced Applications, 7th IFIP
WG 8.8/11.2 International Conference, CARDIS 2006, Tarragona,
Spain, April 19-21, 2006, Proceedings},
booktitle = {CARDIS},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3928},
year = {2006},
isbn = {3-540-33311-8},
bibsource = {DBLP, http://dblp.uni-trier.de}
}