english version Toutes les publications de l'équipe
Publications complete en format BibTeX
[Bibliographie en clair]

complete.bib





@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}
}
@INPROCEEDINGS{HuismanP08,
  author = {Marieke Huisman and Gustavo Petri},
  title = {{BicolanoMT}: a formalization of multi-threaded {Java} at bytecode level},
  year = 2008,
  booktitle = {Bytecode 2008},
  editors = {F. Logozzo and J. Vitek},
  series = {Electronic Notes in Theoretical Computer Science},
  topics = {team},
  pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/bytecode.pdf}
}
@TECHREPORT{Gur-Hui-TR-07,
  author = {D. Gurov and M. Huisman},
  institution = {KTH Royal Institute of Technology, Stockholm},
  number = {TRITA-CSC-TCS 2007:3},
  title = {Reducing Behavioural to Structural Properties of Programs 
	         with Procedures},
  pdfurl = {http://www.csc.kth.se/~dilian/Papers/techrep-07-3.pdf},
  year = 2007,
  topics = {team},
  url = {http://www.nada.kth.se/~dilian/Papers/techrep-07-3.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{HuismanH07,
  author = {Marieke Huisman and Cl\'ement Hurlin},
  title = {The Stability Problem for Verification of Concurrent Object-Oriented Programs},
  booktitle = {Verification and Analysis of Multi-threaded Java-like Programs (VAMP)},
  year = 2007,
  note = {To appear},
  topics = {team},
  pdfurl = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/vamp07.pdf},
  texurl = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/vamp07.tex}
}
@INPROCEEDINGS{HuismanP07,
  author = {Marieke Huisman and Gustavo Petri},
  title = {The {Java} Memory Model: a Formal Explanation},
  booktitle = {Verification and Analysis of Multi-threaded Java-like Programs (VAMP)},
  year = 2007,
  note = {To appear},
  topics = {team},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Gustavo.Petri/publis/jmm-vamp07.pdf}
}
@INPROCEEDINGS{HuismanG07,
  author = {Marieke Huisman and Dilian Gurov},
  title = {Composing Modal Properties of Programs with Procedures},
  booktitle = {Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2007)},
  year = 2007,
  topics = {team},
  pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/fesca.pdf}
}
@INPROCEEDINGS{BurdyHP07,
  author = {Lilian Burdy and Marieke Huisman and Mariela Pavlova},
  title = {Preliminary Design of {BML}: A Behavioral Interface Specification
Language for {Java} bytecode},
  booktitle = {Fundamental Approaches to Software Engineering (FASE 2007)},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = 4422,
  pages = {215-229},
  year = 2007,
  pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/bml.pdf},
  topics = {team}
}
@INPROCEEDINGS{Hurlin:2006:avocs,
  author = {Cl\'ement Hurlin},
  title = {Proof reconstruction for first-order logic and set-theoretical constructions},
  booktitle = {\href{http://avocs06.loria.fr/}{International Workshop on Automated Verification of Critical Systems (AVOCS)}},
  editor = {Stefan Merz and Tobias Nipkow},
  pages = {157--162},
  year = {2006},
  pdfurl = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/avocs06.pdf},
  texurl = {http://www-sop.inria.fr/everest/Clement.Hurlin/publis/avocs06.tex},
  topics = {team}
}
@MISC{inspired:D91,
  author = {Everest Team},
  title = {Developer Oriented Methodology for Applet Validation},
  note = {Inspired Deliverable 9.1.},
  year = {2006},
  topics = {team}
}
@INPROCEEDINGS{BBCGHLPR07:FMCO,
  author = {G. Barthe and L. Burdy and J. Charles and B. Gr{\'e}goire and M. Huisman and J.-L. Lanet and M. Pavlova and A. Requet},
  title = {{JACK}:  a tool for validation of security and behaviour of {Java} applications},
  booktitle = {FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  year = {2007},
  note = {To appear},
  pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/fmco06.pdf},
  topics = {team}
}
@INPROCEEDINGS{Charles:ftfjp06,
  author = {J. Charles},
  title = {Adding Native Specifications to {JML}},
  booktitle = {Proceedings of the ECOOP workshop on Formal Techniques for {Java}-like Programs (FTfJP'2006)},
  psurl = {http://www-sop.inria.fr/everest/personnel/Julien.Charles/papers/06-07-10-ftfjp06-paper.ps},
  year = 2006,
  topics = {team}
}
@INPROCEEDINGS{bgp:lpar06,
  author = {G. Barthe and B. Gr\'egoire and F. Pastawski},
  title = { Type-based termination of recursive definitions in the Calculus of Inductive Constructions},
  topics = {team},
  booktitle = {Proceedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'06)},
  series = {Lecture Notes in Artificial Intelligence},
  year = 2006,
  month = {November},
  publisher = {Springer-Verlag},
  psurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/CICsombrero.ps.gz},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/CICsombrero.pdf.gz},
  note = {To appear}
}
@INPROCEEDINGS{Barthe:Gregoire:Kunz:Rezk:sas06,
  author = {G. Barthe and B. Gr{\'e}goire and C. Kunz 
            and T. Rezk},
  title = {Certificate Translation for Optimizing Compilers},
  booktitle = {Proceedings of the 13th International Static Analysis 
               Symposium (SAS)},
  year = {2006},
  publisher = {Springer-Verlag},
  series = {LNCS},
  address = {Seoul, Korea},
  month = {August},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Cesar.Kunz/publications/certtrans-SAS06.pdf},
  topics = {team}
}
@INPROCEEDINGS{Barthe:Kunz:esop08,
  author = {G. Barthe and C. Kunz},
  title = {Certificate Translation in Abstract Interpretation},
  booktitle = {Proceedings of the 17th European Symposium on Programming (ESOP)},
  year = {2008},
  publisher = {Springer-Verlag},
  series = {LNCS},
  address = {Budapest, Hungary},
  month = {March-April},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Cesar.Kunz/publications/ESOP08.pdf},
  topics = {team}
}
@INPROCEEDINGS{Barthe:Kunz:foal08,
  author = {G. Barthe and C. Kunz},
  title = {Certificate Translation for Specification-Preserving Advices},
  booktitle = {Proceedings of the Foundations of Aspect-Oriented Languages Workshop (FOAL)},
  year = {2008},
  publisher = {ACM},
  series = {},
  address = {Brussels, Belgium},
  month = {April},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Cesar.Kunz/publications/FOAL08.pdf},
  topics = {team}
}
@INPROCEEDINGS{Zanella:2006:FAST,
  author = {Santiago {Zanella B{\'e}guelin} and
                 Gustavo Betarte and
                 Carlos Luna},
  title = {A Formal Specification of the {MIDP} 2.0 Security Model},
  booktitle = {Formal Aspects in Security and Trust, Fourth International
                 Workshop, FAST 2006, Hamilton, Ontario, Canada, August 26-27,
                 2006, Revised Selected Papers},
  editor = {Theodosis Dimitrakos and
                 Fabio Martinelli and
                 Peter Y. A. Ryan and
                 Steve A. Schneider},
  series = {Lecture Notes in Computer Science},
  volume = {4691},
  year = {2006},
  pages = {220-234},
  publisher = {Springer-Verlag},
  isbn = {978-3-540-75226-4},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Santiago.Zanella/MIDP/Zanella.2006.FAST.pdf},
  url = {http://dx.doi.org/10.1007/978-3-540-75227-1_15},
  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}
}
@INPROCEEDINGS{HWS06,
  author = {M. Huisman and P. Worah and K. Sunesen},
  title = {A temporal logic characterisation of observational determinism},
  crossref = {csfw06},
  topics = {team},
  pdfurl = {ftp://ftp-sop.inria.fr/everest/personnel/Marieke.Huisman/obsequiv_char.pdf}
}
@INPROCEEDINGS{BP06JSV,
  author = {L. Burdy and M. Pavlova},
  title = {Java Bytecode Specification and Verification},
  booktitle = {proceedings of SAC'06},
  year = 2006,
  publisher = {ACM},
  series = {},
  editor = {L.M. Liebrock},
  topics = {team},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Mariela.Pavlova/bcSpecVerify.pdf}
}
@INPROCEEDINGS{gdt06:sp,
  author = {G. Barthe and D. Naumann and T. Rezk},
  title = { Deriving an Information Flow Checker and Certifying Compiler for {Java}},
  year = {2006},
  crossref = {sp06},
  psurl = {http://www-sop.inria.fr/everest/personnel/Tamara.Rezk//publication/Barthe-Naumann-Rezk.ps},
  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{gg05:fosad,
  author = {G. Barthe and G. Dufay},
  title = {{Formal methods for smartcard security}},
  pages = {133--177},
  crossref = {fosad05},
  pdfurl = {ftp://ftp-sop.inria.fr/lemme/personnel/Gilles.Barthe/fosad05.pdf},
  topics = {team}
}
@INPROCEEDINGS{BFPR06:flops,
  author = {G. Barthe and  J. Forest and  D. Pichardie and V. Rusu},
  title = {{Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant}},
  pages = {114-129},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/David.Pichardie/Publis/genfixpoint.pdf},
  psurl = {http://www-sop.inria.fr/everest/personnel/David.Pichardie/Publis/genfixpoint.ps.gz},
  topics = {team},
  crossref = {flops06}
}
@INPROCEEDINGS{GTW:flops,
  author = {B. Gr\'egoire and L. Thery and B. Werner},
  title = {A computational approach to {Pocklington} certificates in type 
theory},
  topics = {team},
  pages = {97 - 113},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/pock.pdf},
  crossref = {flops06}
}
@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{gmg05:sefm,
  author = {G. Barthe and M. Pavlova and G. Schneider},
  title = {{Precise analysis of memory consumption using program logics}},
  crossref = {sefm05},
  pages = {86--95},
  pdfurl = {ftp://ftp-sop.inria.fr/lemme/personnel/Gilles.Barthe/sefm2005.pdf},
  topics = {team}
}
@INPROCEEDINGS{gta05:fast,
  author = {G. Barthe and T. Rezk and A. Saabas},
  title = {{Proof obligations preserving compilation}},
  year = {2005},
  crossref = {fast05},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Tamara.Rezk//publication/Barthe-Rezk-Saabas.pdf},
  pages = {112-126},
  topics = {team}
}
@INPROCEEDINGS{sab05:esorics,
  title = {Machine-Checked Security Proofs of Cryptographic
Signature Schemes},
  pages = {140-158},
  author = {S. Tarento},
  crossref = {esorics05},
  topics = {team},
  pdfurl = {http://www-sop.inria.fr/everest/Sabrina.Tarento/Papers/PA/main.pdf}
}
@INPROCEEDINGS{gs04:types,
  title = {A Machine-Checked Formalization of the Random Oracle Model},
  author = {G. Barthe and S. Tarento},
  crossref = {types04},
  topics = {team},
  pdfurl = {http://www-sop.inria.fr/everest/Sabrina.Tarento/Papers/ROM/main.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}
}
@INPROCEEDINGS{BGH02,
  author = {G. Barthe and D. Gurov and M. Huisman},
  title = {Compositional Verification of Secure Applet Interactions},
  crossref = {fase02},
  pages = {15-32},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/fase02.ps.gz},
  topics = {team}
}
@INPROCEEDINGS{CH02,
  author = {N. Cata{\~n}o and M. Huisman},
  title = {Formal specification of {Gemplus'} electronic purse case study using {ESC/Java}},
  pages = {272-289},
  psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/fme37.ps.gz},
  crossref = {fme02},
  topics = {team}
}
@INPROCEEDINGS{HT02,
  author = {K. Trentelman and M. Huisman},
  title = {Extending {JML} Specifications with Temporal Logic},
  crossref = {amast02},
  pages = {334-348},
  psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/amast02.ps.gz},
  topics = {team}
}
@INPROCEEDINGS{Hui-cats05,
  author = {M. Huisman and K. Trentelman},
  title = {Factorising temporal specifications},
  crossref = {cats05},
  pages = {87--96},
  note = {An earlier version appeared as INRIA Technical Report, nr. RR-5326},
  psurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/factorisation.ps.gz},
  topics = {team}
}
@INPROCEEDINGS{BRW-qapl05,
  author = {G. Barthe and T. Rezk and M. Warnier},
  title = {Preventing Timing Leaks Through Transactional Branching Instructions},
  crossref = {qapl05},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Tamara.Rezk/publication/Barthe-Rezk-Warnier.pdf},
  topics = {team}
}
@INPROCEEDINGS{gbf05:tlca,
  author = {G. Barthe and B. Gr\'egoire and F. Pastawski},
  title = {Practical inference for typed-based termination in a polymorphic setting},
  crossref = {tlca05},
  pages = {71-85},
  topics = {team},
  psurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/Fsombrero.ps.gz}
}
@INPROCEEDINGS{gt05:tldi,
  author = {G. Barthe and T. Rezk},
  title = {Non-interference for a {JVM}-like language},
  crossref = {tldi05},
  pages = {103--112},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2005/BR05tldi.ps.gz}
}
@INPROCEEDINGS{gpt04:csfw,
  author = {G. Barthe and P. D'Argenio and T. Rezk},
  title = {{Secure Information Flow by Self-Composition}},
  crossref = {csfw04},
  pages = {100-114},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2004/BDR04csfw.ps.gz}
}
@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}
}
@INPROCEEDINGS{Bertot-Gregoire-Leroy-04,
  author = {Y. Bertot and B. Gr{\'e}goire and X. Leroy},
  title = {A structured approach to proving compiler optimizations based on dataflow analysis},
  url = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/concert.ps.gz},
  pages = {66 - 81},
  topics = {team},
  crossref = {types04}
}
@INPROCEEDINGS{Gregoire-Mahboubi-05,
  author = {B. Gr{\'e}goire and A. Mahboubi},
  title = {Proving equalities in a commutative ring done right in {Coq}},
  crossref = {tphol05},
  url = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/newring.ps.gz},
  pages = {98--113},
  topics = {team}
}
@INPROCEEDINGS{Gregoire-Barras-05,
  author = {B. Barras and B. Gr{\'e}goire},
  title = {On the role of type decorations in the Calculus of Inductive Constructions},
  topics = {team},
  url = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/equiv.ps.gz},
  pages = {151-166},
  crossref = {csl05}
}
@INPROCEEDINGS{BRL-JACK,
  author = {L. Burdy and A. Requet and J.-L. Lanet},
  title = {Java Applet Correctness: A Developer-Oriented Approach},
  crossref = {fme03},
  pages = {422--439},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2003/BRL03fme.ps.gz},
  topics = {team}
}
@INPROCEEDINGS{Betal-JML_Overv,
  author = {L. Burdy and Y. Cheon and D. Cok and M. Ernst and J. Kiniry and G. T. Leavens and K. R. M. Leino and E. Poll},
  title = {An overview of JML tools and applications},
  crossref = {fmics03},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2003/BCCEKLLP03fmics.ps.gz},
  topics = {team}
}
@INPROCEEDINGS{BR-B_control_fl,
  author = {L. Burdy and A. Requet},
  title = {Extending {B} with control flow breaks},
  pages = {513--527},
  crossref = {zb03},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2003/BR03zbex.ps.gz},
  topics = {team}
}
@INPROCEEDINGS{memocode04,
  author = {C. Sprenger and D. Gurov and M. Huisman},
  title = {Compositional Verification for Secure Loading of Smart Card Applets},
  crossref = {memocode04proc},
  pages = {211--222},
  psurl = {http://www.nada.kth.se/~dilian/Papers/memocode04.ps.gz},
  note = {An earlier version appeared as INRIA Technical Report RR-4890},
  topics = {team}
}
@INPROCEEDINGS{gjs04:ijcar,
  author = {G. Barthe and J. Cederquist and S. Tarento},
  title = {{A Machine-Checked Formalization of the Generic Model
and the Random Oracle Model}},
  crossref = {ijcar04},
  pages = {385-399},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2004/BCT04ijcar.ps.gz},
  topics = {team}
}
@INPROCEEDINGS{CH03,
  author = {N. Cata{\~n}o and M. Huisman},
  title = {Chase: A Static Checker for {JML}'s Assignable Clause},
  pages = {26--40},
  psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/vmcai.ps.gz},
  crossref = {vmcai03},
  topics = {team}
}
@INPROCEEDINGS{nestorcatano03s,
  author = {N. Cata{\~n}o},
  title = {Slicing Event Spaces: Towards a {Java} Programs Checking Framework},
  crossref = {fmics03},
  topics = {team}
}
@INPROCEEDINGS{m+04:cardis,
  author = {M. Pavlova and G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet},
  title = {Enforcing High-Level Security Properties For Applets},
  crossref = {cardis04},
  pages = {},
  topics = {team},
  pdfurl = {ftp://ftp-sop.inria.fr/everest/publis/P+04cardis.pdf}
}
@INPROCEEDINGS{gl04:fmse,
  author = {G. Barthe and L. Prensa-Nieto},
  title = {Formally Verifying Information Flow Type Systems for
Concurrent and Thread Systems},
  crossref = {fmse04},
  pages = {13-22},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2004/BP04fmse.ps.gz}
}
@INPROCEEDINGS{gg04:fase,
  author = {G. Barthe and G. Dufay},
  title = {{A Tool-Assisted Framework for Certified Bytecode 
Verification}},
  pages = {99-113},
  crossref = {fase04},
  topics = {team,castles},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2004/BD04fase.ps.gz}
}
@INPROCEEDINGS{HuismanGSC03,
  author = {M. Huisman and D. Gurov and C. Sprenger and G. Chugunov},
  title = {Checking Absence of Illicit Applet Interactions: a Case Study},
  pages = {84-98},
  crossref = {fase04},
  psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/casestudy.ps.gz},
  topics = {team}
}
@INPROCEEDINGS{gat04:vmcai,
  author = {G. Barthe and A. Basu and T. Rezk},
  title = {Security Types Preserving Compilation},
  crossref = {vmcai04},
  pages = {2--15},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2004/BBR04vmcai.ps.gz}
}
@INPROCEEDINGS{gs03:rta,
  author = {G. Barthe and S. Stratulat},
  title = {{Using Implicit Induction Techniques for the Validation of
the JavaCard Platform}},
  crossref = {rta03},
  pages = {337 - 351},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/rta03.ps.gz}
}
@INPROCEEDINGS{g+03:popl,
  author = {G. Barthe and H. Cirstea and C. Kirchner and L. Liquori},
  title = {Pure Pattern Type Systems},
  crossref = {popl03},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/popl03.ps.gz}
}
@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}
}
@ARTICLE{gat05:cl,
  author = {G. Barthe and  T. Rezk and A. Basu},
  title = {Security Types Preserving Compilation},
  year = {200x},
  journal = {Journal of Computer Languages, Systems and Structures},
  pdfurl = {http://www-sop.inria.fr/everest/Tamara.Rezk/publication/Barthe-Rezk-Basu.Journal.pdf},
  topics = {team},
  note = {To appear}
}
@ARTICLE{gt04:jfp,
  author = {G. Barthe and T. Coquand},
  title = {On the equational theory of non-normalizing Pure Type Systems},
  journal = {{Journal of Functional Programming}},
  year = {2004},
  volume = 14,
  number = 2,
  pages = {191--209},
  month = MAR,
  psurl = {ftp://ftp-sop.inria.fr/everest/Gilles.Barthe/fix.ps.gz},
  topics = {team}
}
@ARTICLE{g+04:mscs,
  author = {G. Barthe and M. J. Frade  and E. Gim{\'e}nez and L. Pinto
and T. Uustalu},
  title = {Type-Based Termination of Recursive Definitions},
  year = {2004},
  journal = {{Mathematical Structures in Computer Science}},
  month = FEB,
  volume = 14,
  issue = 1,
  pages = {97--141},
  psurl = {ftp://ftp-sop.inria.fr/everest/Gilles.Barthe/tbt.ps.gz},
  topics = {team}
}
@ARTICLE{g04:mscs,
  author = {G. Barthe},
  title = {Type Isomorphisms and Back-and-Forth Coercions in Type 
Theory},
  year = {2005},
  journal = {{Mathematical Structures in Computer Science}},
  topics = {team}
}
@ARTICLE{BCR-TSI,
  author = {L. Burdy and L. Casset and A. Requet},
  title = {D{\'e}veloppement d'un v{\'e}rifieur de byte-code embarqu{\'e}},
  journal = {Technique et Science Informatiques},
  volume = {22},
  number = {1},
  year = {2003},
  pages = {33--60},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2003/BCR03ver.ps.gz},
  topics = {team}
}
@ARTICLE{final:Form.Met,
  author = {C. Breunesse and N. Cata{\~n}o and M. Huisman and B. Jacobs},
  title = {Formal Methods for Smart Cards: an experience report},
  journal = {Science of Computer Programming},
  year = {2005},
  volume = 55,
  number = {1-3},
  pages = {53-80},
  pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/fm_smart.pdf},
  topics = {team}
}
@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{gdphd,
  author = {G. Dufay},
  title = {V\'erification formelle de la plate-forme Java Card},
  school = {Universit\'e de Nice Sophia-Antipolis},
  month = {December},
  year = {2003},
  url = {http://www-sop.inria.fr/lemme/personnel/Guillaume.Dufay/these/},
  pdfurl = {http://www-sop.inria.fr/lemme/personnel/Guillaume.Dufay/these/these-gdufay.pdf},
  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 }
}
@MASTERSTHESIS{Tar03,
  author = {S. Tarento},
  title = {Certifying  cryptographic algorithms using the Coq system},
  school = {Universit\'e de Nice},
  year = {2003},
  type = {Rapport de DEA},
  topics = {team},
  url = {http://www-sop.inria.fr/everest/Sabrina.Tarento/Papers/rapport.dvi}
}
@MASTERSTHESIS{Pav03,
  author = {M. Pavlova},
  title = {Automatic generation of JML specification  for Java Card applications},
  school = {Universit\'e Paris VII - Denis Diderot},
  year = {2003},
  type = {Rapport de DEA},
  topics = {team},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Mariela.Pavlova/Rapport.pdf}
}
@MASTERSTHESIS{Duf00,
  author = {G. Dufay},
  title = {Formalisation en Coq de la Machine Virtuelle JavaCard},
  school = {Universit\'e Paris VII - Denis Diderot},
  year = {2000},
  type = {Rapport de DEA},
  psurl = {http://www-sop.inria.fr/everest/personnel/Guillaume.Dufay/DEA-dufay.ps.gz},
  topics = {team}
}
@MASTERSTHESIS{Cha05,
  author = {J. Charles},
  title = {V\'erification d'un composant {Java}: Le v\'erificateur de bytecode},
  school = {Universit\'e de Nice},
  year = {2005},
  psurl = {http://www-sop.inria.fr/everest/personnel/Julien.Charles/papers/05-06-17-rapport.ps},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Julien.Charles/papers/05-06-17-rapport.pdf},
  topics = {team}
}
@TECHREPORT{BreunesseCHJ03,
  author = {C. Breunesse and N. Cata{\~n}o and M. Huisman and B. Jacobs},
  title = {{Formal Methods for Smart Cards: an experience report}},
  number = {NIII-R0316},
  institution = {NIII},
  year = {2003},
  url = {http://www.cs.kun.nl/research/reports/info/NIII-R0316.html},
  topics = {team}
}
@TECHREPORT{SprengerGH03,
  author = {C. Sprenger and D. Gurov and M. Huisman},
  title = {Simulation Logic, Applets and Compositional Verification},
  number = {RR-4890},
  institution = {INRIA},
  year = {2003},
  psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/techreport.ps.gz},
  topics = {team}
}
@TECHREPORT{mariela+03,
  author = {M. Pavlova and G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet},
  title = {Enforcing High-Level Security Properties For Applets},
  number = {RR-5061},
  institution = {INRIA},
  year = {2003},
  url = {http://www-sop.inria.fr/rapports/sophia/RR-5061.html},
  topics = {team}
}
@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}
}
@TECHREPORT{GH-5330,
  author = {D. Gurov and M. Huisman},
  title = {Abstraction over Public Interfaces},
  institution = {INRIA},
  year = {2004},
  number = {RR-5330},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/interfaces_techreport.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{csfw06,
  title = {19th IEEE Computer Security Foundations Workshop},
  booktitle = {19th IEEE Computer Security Foundations Workshop},
  publisher = {IEEE Computer Society},
  month = {July},
  year = 2006
}
@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}
}

This file has been generated by bibtex2html 1.87.

on Tue, 02 Sep 2008 00:00:10 +0200