publis-geccoo.bib

@ARTICLE{marche04jlap,
  author = {Claude March{\'e} and Christine Paulin-Mohring and Xavier Urbain},
  title = {The \textsc{Krakatoa} Tool for Certification of \textsc{Java/JavaCard} Programs annotated in \textsc{JML}},
  journal = {Journal of Logic and Algebraic Programming},
  year = 2004,
  volume = 58,
  number = {1--2},
  pages = {89--106},
  url = {http://krakatoa.lri.fr},
  topics = {team},
  type_publi = {irevcomlec}
}
@INPROCEEDINGS{marche05tphols,
  topics = {team},
  author = {Claude March\'e and Christine Paulin-Mohring},
  title = {Reasoning about {Java} Programs with Aliasing and Frame
  Conditions},
  booktitle = {18th International Conference on Theorem Proving in Higher Order Logics},
  editor = {J. Hurd and T. Melham},
  series = {LNCS},
  year = 2005,
  addresse = {Oxford, UK},
  month = AUG,
  publisher = {Springer-Verlag}
}
@INPROCEEDINGS{marche06sefm,
  author = {Claude March\'e and Nicolas Rousset},
  topics = {team},
  title = {Verification of {Java Card} Applets Behavior with
  respect to Transactions and Card Tears},
  year = 2006,
  editor = {Dang Van Hung and Paritosh Pandya},
  booktitle = {4th IEEE International Conference on Software Engineering
and Formal Methods (SEFM'06)},
  address = {Pune, India},
  month = SEP,
  type_publi = {icolcomlec},
  url = {http://www.lri.fr/~marche/marche06sefm.ps}
}
@MISC{HARVEY,
  author = {David D\'eharbe and Sylvio Ranise},
  title = {{haRVey}},
  year = 2004,
  note = {\url{http://www.loria.fr/~ranise/haRVey}}
}
@MISC{jack04,
  key = {Jack},
  author = {Lilian Burdy and Jean-Louis Lanet and Antoine Requet},
  title = {JACK: Java Applet Correctness Kit},
  year = 2004,
  note = {\url{http://www-sop.inria.fr/everest/soft/Jack/jack.html}}
}
@MISC{why,
  author = {Jean-Christophe Filli{\^a}tre},
  title = {The {Why} certification tool},
  note = {\url{http://why.lri.fr/}}
}
@INPROCEEDINGS{bdg:zb05,
  author = {Bouquet, F. and Dadeau, F. and Groslambert, J.},
  title = {{Checking {JML} Specifications with {B} Machines}},
  booktitle = {Proceedings of the International Conference on Formal Specification and Development in {Z} and {B} (ZB'05)},
  year = {2005},
  address = {Guildford, United Kingdom},
  series = {LNCS},
  publisher = {Springer-Verlag},
  month = APR,
  editors = {H. Treharne, S. King, M. Henson and S. Schneider},
  volume = {3455},
  pages = {435-454}
}
@INPROCEEDINGS{bdlu:tacas05,
  author = {Bouquet, F. and Dadeau, F. and Legeard, B. and Utting, M.},
  title = {{JML}-Testing-Tools: a Symbolic Animator for {JML} Specifications using {CLP}},
  booktitle = {Proceedings of 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Tool session (TACAS'05)},
  address = {Edinburgh, United Kingdom},
  publisher = {Springer-Verlag},
  editors = {N. Halbwachs and L. Zuck},
  volume = {3440},
  pages = {551-556},
  series = {LNCS},
  year = {2005},
  month = {April}
}
@INPROCEEDINGS{bdlu:fme05,
  author = {Bouquet, F. and Dadeau, F. and Legeard, B. and Utting, M.},
  title = {Symbolic Animation of {JML} Specifications},
  booktitle = {Proceedings of the International Conference on Formal
             Methods (FM'2005)},
  address = {Newcastle Upon Tyne, United Kingdom},
  publisher = {Springer-Verlag},
  series = {LNCS},
  year = {2005},
  editors = {J.S. Fitzgerald, I.J. Hayes, and A.~Tarlecki},
  month = {July},
  volume = {3582},
  pages = {75--90}
}
@INCOLLECTION{bck04:bc,
  author = {Bellegarde, F. and Charlet, C. and Kouchnarenko, O.},
  title = {How to Compute the Refinement Relation for Parameterized Systems},
  booktitle = {Formal Methods and Models for System Design},
  year = 2004,
  chapter = 2,
  publisher = {Springer-Verlag},
  editor = {Gupta, R. and Le Guenic P. and Talpin J.P.}
}
@TECHREPORT{StoulsCC,
  author = {Nicolas Stouls },
  title = {{Documentation d'introduction aux crit\`eres communs}},
  institution = {LSR laboratory},
  note = {\\ http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/Productions/CC/CriteresCommuns.pdf},
  year = {2004}
}
@PROCEEDINGS{B2007,
  title = {The 7th International B Conference (B'2007)},
  year = 2007,
  booktitle = {The 7th International B Conference (B'2007)},
  editor = {Jacques Julliand and Olga Kouchnarenko},
  volume = 4355,
  series = {LNCS},
  publisher = {Springer-Verlag}
}
@INPROCEEDINGS{SP07,
  author = {Nicolas Stouls and Marie-Laure Potet},
  title = {{Security Policy Enforcement Through Refinement Process}},
  crossrefs = {B2007},
  pages = {216--231},
  year = 2007
}
@INPROCEEDINGS{BoulmePotet07,
  author = {Sylvain Boulm\'e and Marie-Laure Potet},
  title = {{Interpreting invariant composition in the B method using the Spec\# ownership
relation: a way to explain and relax B restrictions}},
  crossref = {B2007},
  year = 2007
}
@INPROCEEDINGS{MorselliPotetStouls04,
  author = {Xavier Morselli and Marie-Laure Potet and Nicolas Stouls},
  title = {G\'en\'eSyst : G\'en\'eration d'un syst\`eme de transitions \'etiquet\'ees \`a partir d'une sp\'ecification {{B}} \'ev\'enementiel},
  booktitle = {AFADL'2004},
  pages = {317--320},
  year = 2004,
  month = JUN,
  url = {http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/Productions/2004_Afadl_GeneSyst/GeneSyst_SessionOutils.ps.gz}
}
@INPROCEEDINGS{BPS06,
  author = {D. Bert and M-L. Potet and N. Stouls},
  title = {{GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications.
Application to Security Properties}},
  booktitle = {ZB 2005: Formal Specification and Development in Z and B, 4th International
Conference of B and Z Users},
  editor = {H.{~}Treharne and S.{~}King and M.{~}C.{~}Henson and S.{~}A.{~}Schneider},
  publisher = {Springer-Verlag},
  series = {LNCS},
  volume = {3455},
  pages = {299--318},
  year = 2005,
  isbn = {3-540-25559-1}
}
@INPROCEEDINGS{PotetStouls04,
  author = {Marie-Laure Potet and Nicolas Stouls},
  title = {Explicitation du contr\^ole de d\'eveloppement {{B}} \'ev\'enementiel},
  booktitle = {AFADL'2004},
  pages = {13--27},
  editor = {J.{~}Julliand},
  year = 2004,
  month = JUN,
  url = {http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/Productions/2004_Afadl_GeneSyst/Article_Afadl-NS_et_MLP.ps.gz}
}
@TECHREPORT{haddad05,
  author = {Amal Haddad},
  title = {{Mod\'elisation et v\'erification de politiques de s\'ecurit\'e}},
  institution = {LSR laboratory},
  note = {\\ http://www-lsr.imag.fr/Les.Personnes/Marie-Laure.Potet/PUBLI/DEA\_Amal\_HADDAD.pdf},
  year = {2005}
}
@INPROCEEDINGS{Haddad07,
  author = {Amal Haddad},
  title = {{Meca: a tool for Access Control Models}},
  crossref = {B2007},
  year = 2007,
  note = {Tool session},
  url = {\\ http://www-lsr.imag.fr/Les.Personnes/Marie-Laure.Potet/PUBLI/MecaB.pdf}
}
@INPROCEEDINGS{genesyst05,
  author = {Didier Bert and Marie-Laure Potet and Nicolas Stouls},
  title = {G\'en\'eSyst: a Tool to Reason about Behavioral Aspects of {B Event Specifications}. Application to Security Properties},
  booktitle = {Proceedings of the International Conference on Formal Specification and Development in {Z} and {B} (ZB'05)},
  year = {2005},
  address = {Guildford, United Kingdom},
  series = {LNCS},
  publisher = {Springer-Verlag},
  month = APR,
  editors = {H. Treharne, S. King, M. Henson and S. Schneider},
  volume = {3455},
  pages = {299-318}
}
@INCOLLECTION{armando04siekmann,
  author = {A. Armando and L. Compagna and S. Ranise},
  booktitle = {Mechanizing Mathematical Reasoning. Essays in Honor of J. H. Siekmann on the Occasion of his 60th Birthday},
  title = {Rewriting and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation},
  pages = {30--45},
  publisher = {Springer-Verlag},
  year = 2005,
  editor = {Dieter Hutter and Werner Stephan},
  volume = 2605,
  series = {LNAI}
}
@ARTICLE{ARR03,
  author = {A, Alessandro and Ranise, S. and
                  Rusinowitch, Micha{\"e}l},
  title = {A rewriting approach to satisfiability procedures},
  journal = {Information and Computation},
  volume = {183},
  number = {2},
  pages = {140--164},
  year = {2003}
}
@INPROCEEDINGS{TZ04,
  author = {Tinelli, Cesare and
             Zarba, Calogero G.},
  title = {Combining Decision Procedures for Sorted Theories},
  editor = {Alferes, Jos{\'e} J{\'u}lio and
             Leite, Jo{\~a}o Alexandre},
  booktitle = {Logics in Artificial Intelligence},
  volume = {3229},
  series = {Lecture Notes in Computer Science},
  pages = {641--653},
  publisher = {Springer-Verlag},
  year = {2004}
}
@INPROCEEDINGS{FRZ05,
  author = {Pascal Fontaine and Silvio Ranise and Calogero
                  G. Zarba},
  title = {Combining lists with non-stably infinite theories},
  editor = {Franz Baader and Andrei Voronkov},
  booktitle = {Logic for Programming, Artificial Intelligence, and
                  Reasoning},
  series = {Lecture Notes in Computer Science},
  volume = {3452},
  pages = {51--66},
  publisher = {Springer-Verlag},
  year = {2005}
}
@INPROCEEDINGS{ictac04,
  author = {Ranise, Silvio and Ringeissen, Christophe and Tran, Duc-Khanh},
  title = {{Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture
  with a Newborn}},
  booktitle = {{First International Colloquium on Theoretical Aspects of
  Computing - ICTAC 2004}},
  editor = {Araki, Keijiro and Liu, Zhiming},
  address = {Guiyang, Chine},
  month = SEP,
  publisher = {Springer-Verlag},
  series = {LNCS},
  year = {2004},
  note = {In post-event proceedings. Also available as Research Report
  A04-R-193, LORIA, France}
}
@ARTICLE{ZCS05,
  author = {Zarba, Calogero G. and 
                  Cantone, Domenico and
                  Schwartz, Jacob T.},
  title = {A decision procedure for a sublanguage of set theory
                  involving monotone, additive, and multiplicative
                  functions, {I}. {T}he: two-level case},
  journal = {Journal of Automated Reasoning},
  year = {2004},
  volume = 33,
  number = {3-4},
  pages = {251-269}
}
@ARTICLE{TZ05,
  author = {Tinelli, Cesare and Zarba, Calogero G.},
  title = {Combining non-stably infinite theories},
  journal = {Journal of Automated Reasoning},
  year = 2005,
  volume = 34,
  number = 3,
  pages = {209-238}
}
@INPROCEEDINGS{aisc04,
  author = {Imine, A. and D\'eharbe, D. and Ranise, S.},
  title = {{Abstraction-Driven Verification of Array Programs}},
  booktitle = {Proceedings of the 7th International Conference on Artificial
  Intelligence and Symbolic Computation (AISC'04)},
  address = {Linz, Austria},
  month = SEP,
  number = {3249},
  pages = {271--275},
  publisher = {Springer-Verlag},
  series = {LNCS},
  year = {2004}
}
@INPROCEEDINGS{sefm03,
  author = {D\'eharbe, D. and Ranise, S.},
  title = {{Light-Weight Theorem Proving for Debugging and Verifying Units of
  Code}},
  booktitle = {Proc. of the International Conference on Software Engineering and
  Formal Methods (SEFM03)},
  address = {Brisbane, Australia},
  month = {September},
  publisher = {IEEE Computer Society Press},
  year = {2003},
  url = {http://www.loria.fr/~ranise/pubs/sefm03.ps.gz}
}
@INPROCEEDINGS{pdpar04,
  author = {F. Mehta and S. Ranise},
  title = {Automated Provers doing (Higher-Order) Proof search: A Case Study in the Verification of Pointer Programs},
  booktitle = {Proc.\@ of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR'04)},
  year = 2004
}
@INPROCEEDINGS{wmf03,
  author = {Couchot, J.-F. and Dadeau, F. and D\'eharbe, D. and Giorgetti, A.
  and Ranise, S.},
  title = {Proving and Debugging Set-Based Specifications},
  booktitle = {Electronic Notes in Theoretical Computer Science, proceedings of
  the Sixth Brazilian Workshop on Formal Methods (WMF'03)},
  editor = {Cavalcanti, A. and Machado, P.},
  address = {Campina Grande, Brazil},
  month = {May},
  pages = {189--208},
  volume = {95},
  year = {2004},
  url = {http://dx.doi.org/10.1016/j.entcs.2004.04.012}
}
@ARTICLE{jbcs04,
  author = {Couchot, J.-F. and D\'eharbe, D. and Giorgetti, A. and Ranise, S.},
  title = {Scalable Automated Proving and Debugging of Set-Based
  Specifications},
  journal = {Journal of the Brazilian Computer Society},
  month = {November},
  number = {2},
  pages = {17--36},
  volume = {9},
  year = {2003},
  note = {ISSN 0104-6500},
  url = {http://lifc.univ-fcomte.fr/~couchot/pubs/cdgr04.ps.gz}
}
@INPROCEEDINGS{StoulsDarmaillacq06,
  author = {Nicolas Stouls and Vianney Darmaillacq},
  title = {{D\'eveloppement formel d'un moniteur d\'etectant les violations de politiques de
s\'ecurit\'e de r\'eseaux}},
  booktitle = {Approches Formelles dans l'Assistance au D\'eveloppement de Logiciels (AFADL'06)},
  pages = {179--193},
  editor = {S.{~}Vignes and V.{~}Vigui\'e Donzeau-Gouge},
  year = 2006,
  month = MAR,
  note = {http://www-lsr.imag.fr/Les.Personnes/Nicolas.Stouls/Productions/2005-09-AFADL06/AFADL06.pdf}
}
@INPROCEEDINGS{cdgr04:np,
  author = {Couchot, J.-F. and D\'eharbe, D. and Giorgetti, A. and 
Ranise, S.},
  title = {{B}arvey~: {V}\'erification automatique de consistance de 
machines abstraites {B}},
  pages = {369--372},
  booktitle = {Sessions Outils, Congr\`es Approches Formelles dans 
l'Assistance au D\'eveloppement de Logiciels, AFADL'04},
  address = {Besan\c{c}on, France},
  month = JUN,
  year = 2004,
  editor = {Julliand, J.},
  url = {http://lifc.univ-fcomte.fr/~couchot/pubs/cdgr04b.ps.gz}
}
@INPROCEEDINGS{cg04:np,
  author = {Couchot, J.-F. and Giorgetti, A.},
  title = {Analyse d'atteignabilit\'e d\'eductive},
  booktitle = {Congr\`es Approches Formelles dans l'Assistance au 
D\'eveloppement de Logiciels, AFADL'04},
  pages = {269--283},
  editor = {Julliand, J.},
  address = {Besan\c{c}on, France},
  month = JUN,
  year = 2004,
  url = {http://lifc.univ-fcomte.fr/~couchot/pubs/cg04.ps.gz}
}
@TECHREPORT{dg03:ir,
  author = {Dadeau, F. and Giorgetti, A.},
  title = {V\'erification de machines abstraites {B} en logique 
monadique du second ordre},
  institution = {LIFC - Laboratoire d'{I}nformatique de 
l'{U}niversit\'{e} de {F}ranche {C}omt\'{e}},
  type = {Rapport de Recherche},
  pdf = {/publis/pub/2003/RR2003-01.pdf},
  number = {RR2003-01},
  month = OCT,
  year = 2003,
  pages = {1--29}
}
@ARTICLE{cjmb04:ij,
  author = {Chouali, S. and Julliand, J. and Masson, P.-A. and Bellegarde, F.},
  title = {{PLTL} {P}artitionned {M}odel-{C}hecking for {R}eactive {S}ystems under {F}airness {A}ssumptions},
  journal = {ACM - Transactions in Embedded Computing Systems (TECS)},
  year = 2005,
  volume = 4,
  number = 2,
  pages = {267-301}
}
@TECHREPORT{technical-report-liveness,
  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,
  key = {RR-5331}
}
@TECHREPORT{chaudhary04demoney,
  author = {Vikrant Chaudhary},
  title = {The {Krakatoa} tool for certification of {Java/JavaCard} 
programs annotated in {JML} : A Case Study},
  institution = {IIT internship report},
  year = 2004,
  month = JUL
}
@TECHREPORT{boulmeho,
  author = {Sylvain Boulm\'e},
  title = {{Specifying and reasoning in Coq with high-order impure programs using
specifications a la Dijkstra and refinement}},
  institution = {LSR laboratory},
  note = {\\ http://www-lsr.imag.fr/Les.Personnes/Sylvain.Boulme/horefinement},
  year = {2006}
}
@INPROCEEDINGS{pavlova04,
  author = {M. Pavlova and G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet},
  title = {Enforcing High-Level Security Properties For Applets},
  booktitle = {CARDIS'04},
  year = 2004,
  editor = {J.-J. Quisquater and P. Paradinas and Y. Deswarte and A.A. El Kalam},
  publisher = {Kluwer},
  note = {An earlier version appeared as INRIA Technical Report, nr. RR-5061}
}
@ARTICLE{Breunesse05,
  author = {C.-B. Breunesse and N. Catan~o and M. Huisman and B.P.F. 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}
}
@INPROCEEDINGS{gpt04:csfw,
  author = {Gilles Barthe and Pedro R. D'Argenio and Tamara Rezk},
  title = {{Secure Information Flow by Self-Composition}},
  booktitle = {17th IEEE Computer Security Foundations Workshop (CSFW'04)},
  pages = {100-114},
  topics = {team},
  publisher = {IEEE Computer Society},
  address = {Los Alamitos, CA, USA},
  year = {2004},
  editor = {R. Foccardi},
  month = {June},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2004/BDR04csfw.ps.gz}
}
@INPROCEEDINGS{gmg05:sefm,
  author = {G. Barthe and M. Pavlova and G. Schneider},
  title = {{Precise analysis of memory consumption using program logics}},
  pdfurl = {ftp://ftp-sop.inria.fr/lemme/personnel/Gilles.Barthe/sefm2005.pdf},
  year = {2005},
  booktitle = {Proceedings of SEFM'05},
  editor = {B.~Aichernig and B.~Beckert},
  publisher = {IEEE Press}
}
@INPROCEEDINGS{burdysac06,
  author = {Lilian Burdy and Mariela Pavlova},
  title = {Java Bytecode Specification and Verification},
  booktitle = {21st Annual ACM Symposium on Applied Computing (SAC'06)},
  year = 2006,
  address = {Dijon},
  editor = {L.M.~Liebrock},
  month = APR,
  publisher = {ACM Press}
}
@INPROCEEDINGS{frocos05-ABRS,
  author = {Armando, A. and Bonacina, M. P. and Ranise, S. and Schulz, S.},
  title = {{On a rewriting approach to satisfiability procedures: extension,
  combination of theories and an experimental appraisal}},
  booktitle = {Proc. of the 5th Int. Workshop on Frontiers of Combining Systems
  (FroCoS'2005)},
  editor = {Gramlich, B.},
  address = {Vienna, Austria},
  month = {September},
  pages = {65--80},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3717},
  year = {2005}
}
@INPROCEEDINGS{isola05,
  author = {D. D{\'e}harbe and S. Ranise},
  title = {{Satisfiability Solving for Software Verification}},
  booktitle = {ISoLA-2005: 2005 IEEE ISoLA Workshop on Leveraging Applications
of Formal Methods, Verification, and Validation},
  year = 2005,
  address = {Columbia, Maryland}
}
@INPROCEEDINGS{ictac05,
  author = {Kirchner, H. and Ranise, S. and Ringeissen, C. and Tran, D.-K.},
  title = {{On Superposition-Based Satisfiability Procedures and their
  Combination}},
  booktitle = {Proc.\@ of the 2nd International Conference on Theoretical
  Aspects of Computing (ICTAC'05)},
  editor = {Van Hung, Dang and Wirsing, Martin},
  address = {Hanoi, Vietnam},
  month = {October},
  pages = {594--608},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3722},
  year = {2005}
}
@ARTICLE{RaniseT-IS06,
  author = {Ranise, S. and Tinelli, C.},
  title = {{Satisfiability Modulo Theories}},
  journal = {IEEE Magazine on Intelligent Systems},
  month = {November},
  year = {2006},
  note = {To appear}
}
@MISC{RanTin-SMTLIB,
  author = {Silvio Ranise and Cesare Tinelli},
  title = {{The Satisfiability Modulo Theories Library (SMT-LIB)}},
  howpublished = {{\tt www.SMT-LIB.org}},
  year = 2006
}
@TECHREPORT{RanTin-RR-06,
  author = {Silvio Ranise and Cesare Tinelli},
  title = {{The SMT-LIB Standard: Version 1.2}},
  institution = {Department of Computer Science, The University of
                  Iowa},
  year = 2006,
  note = {Available at {\tt www.SMT-LIB.org}}
}
@INPROCEEDINGS{ranise-ijcar06,
  author = {Bonacina, M. P. and Ghilardi, S. and Nicolini, E. and Ranise, S. and
  Zucchelli, D.},
  title = {{Decidability and Undecidability Results for Nelson-Oppen and
  Rewrite-Based Decision Procedures}},
  booktitle = {Proc. of the 3rd Int. Conference on Automated Reasoning (IJCAR)},
  address = {Seattle, WA, USA},
  month = {August},
  number = {4130},
  pages = {513--527},
  series = {LNAI},
  year = {2006}
}
@INPROCEEDINGS{ranise-disproving06,
  author = {Ranise, S.},
  title = {{Satisfiability Solving for Program Verification: towards the
  efficient Combination of Automated Theorem Provers and Satisfiability Modulo
  Theory Tools}},
  booktitle = {Proc. of the IJCAR'06 Ws. DISPROVING: Non-Theorems, Non-Validity,
  Non-Provability},
  editor = {Ahrendt, W. and Baumgartner, P. and de Nivelle, H.},
  address = {Seattle, WA, USA},
  month = {August},
  pages = {49--58},
  year = {2006},
  note = {Invited paper}
}
@INPROCEEDINGS{ranise-pdpar06-a,
  author = {Ghilardi, S. and Nicolini, E. and Ranise, S. and Zucchelli, D.},
  title = {{Deciding Extensions of the Theory of Arrays by Integrating Decision
  Procedures and Instantiation Strategies}},
  booktitle = {Proc. of the IJCAR'06 Ws. PDPAR: Pragmatical Aspects of Decision
  Procedures in Automated Reasoning},
  editor = {Cook, B. and Sebastiani, R.},
  address = {Seattle, WA, USA},
  month = {August},
  year = {2006}
}
@INPROCEEDINGS{ranise-sefm06,
  author = {Ranise, S. and Zarba, C.},
  title = {{A Theory of Singly-Linked Lists and its Extensible Decision
  Procedure}},
  booktitle = {Proc. of the 4th IEEE International Conference on Software
  Engineering and Formal Methods (SEFM)},
  address = {Pune, India},
  month = {September},
  publisher = {IEEE Computer Society Press},
  year = {2006},
  note = {Extended version with full proofs, motivations, and examples in a
  technical report available at
  \texttt{\url{http://www.loria.fr/~ranise/pubs}}.}
}
@INPROCEEDINGS{ranise-jelia06,
  author = {Ghilardi, S. and Nicolini, E. and Ranise, S. and Zucchelli, D.},
  title = {{Deciding Extensions of the Theory of Arrays by Integrating Decision
  Procedures and Instantiation Strategies}},
  booktitle = {Proc. of the 10th European Conference on Logics in Artificial
  Intelligence (Jelia)},
  month = {September},
  number = {4160},
  series = {Lecture Notes in Computer Science},
  year = {2006},
  note = {Extended version with full proofs, motivations, and examples in a
  technical report available at \url{http://www.loria.fr/~ranise/pubs}.}
}
@ARTICLE{ranise-ic06,
  author = {Bozzano, M. and Bruttomesso, R. and Cimatti, A. and Junttila, T. and
  van Rossum, P. and Ranise, S. and Sebastiani, R.},
  title = {{Efficient Theory Combination via Boolean Search}},
  journal = {Journal of Information and Computation},
  number = {204},
  pages = {1411-1596},
  volume = {10},
  year = {2006},
  note = {Special Issue on Combining Logical Systems}
}
@INPROCEEDINGS{DucLPAR06,
  author = {Kirchner, H\'el\`ene and Ranise, Silvio and Ringeissen, Christophe
  and Tran, Duc-Khanh},
  title = {{Automatic Combinability of Rewriting-Based Satisfiability
  Procedures}},
  booktitle = {Proc. of the 13th Int. Conference on Logic for Programming,
  Artificial Intelligence, and Reasoning (LPAR'06)},
  address = {Phnom Penh, Cambodia},
  month = NOV,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Artificial Intelligence},
  year = {2006}
}
@INPROCEEDINGS{KirchnerRRT-TFIT06,
  author = {Kirchner, H\'el\`ene and Ranise, Silvio and Ringeissen, Christophe
  and Tran, Duc-Khanh},
  title = {{Building and Combining Satisfiability Procedures for Software
  Verification}},
  booktitle = {Proceedings of 3rd Taiwanese-French Conference on Information
  Technology (TFIT)},
  address = {Nancy, France},
  month = {March},
  pages = {125-139},
  year = {2006}
}
@INPROCEEDINGS{RaniseRT-PDPAR06,
  author = {Ranise, Silvio and Ringeissen, Christophe and Tran, Duc-Khanh},
  title = {{Producing Conflict Sets for Combination of Theories}},
  booktitle = {Pragmatics of Decision Procedures in Automated Reasoning
  (PDPAR)},
  editor = {Cook, B. and Sebastiani, R.},
  address = {Seattle (WA)},
  month = {August},
  year = {2006},
  note = {Workshop affiliated to the 3rd International Joint Conference on
  Automated Reasoning, IJCAR}
}
@INPROCEEDINGS{DeharbeFRR-ICTAC06,
  author = {D\'eharbe, David and Fontaine, Pascal and Ranise, Silvio and
  Ringeissen, Christophe},
  title = {{Decision Procedures for the Formal Analysis of Software}},
  booktitle = {3rd International Colloquium on Theoretical Aspects of Computing,
  ICTAC},
  address = {Tunis, Tunisia},
  month = {November},
  publisher = {Springer},
  volume = {4281},
  series = {Lecture Notes in Computer Science},
  year = {2006},
  note = {Tutorial}
}
@INPROCEEDINGS{ftp05,
  author = {Boughanmi, N. and Ranise, S. and Ringeissen, C.},
  title = {{On Structural Information and the Experimental Evaluation of SMT
  Tools}},
  booktitle = {Proc. of the International Workshop on First-Order Theorem
  Proving (FTP'05)},
  address = {Koblenz, Germany},
  year = {2005}
}
@INPROCEEDINGS{pdpar05,
  author = {Armando, A. and Bonacina, M. P. and Ranise, S. and Schulz, S.},
  title = {Big proof engines as little proof engines: new results on
  rewrite-based satisfiability procedures (Extended abstract)},
  booktitle = {Notes of the Third Workshop on Pragmatics of Decision Procedures
  in Automated Reasoning (PDPAR), co-located with CAV'05},
  address = {Edinburgh, Scotland (UK)},
  year = {2005}
}
@INPROCEEDINGS{frocos05b,
  author = {Ranise, S. and Ringeissen, C. and Zarba, C. G.},
  title = {{Combining data structures with nonstably infinite theories using
  many-sorted logic}},
  booktitle = {Proc. of the 5th Int. Workshop on Frontiers of Combining Systems
  (FroCoS'2005)},
  editor = {Gramlich, B.},
  address = {Vienna, Austria},
  month = {September},
  pages = {48--64},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3717},
  year = {2005}
}
@INPROCEEDINGS{cav05,
  author = {Bozzano, M. and Bruttomesso, R. and Cimatti, A. and Junttila, T. and
  van Rossum, P. and Ranise, S. and Sebastiani, R.},
  title = {{Efficient Satisfiability Modulo Theories via Delayed Theory
  Combination}},
  booktitle = {Proc. of the Int. Conf. on Computer-Aided Verification (CAV
  2005)},
  publisher = {Springer-Verlag},
  address = {Edinburg, Scotland (UK)},
  number = {3576},
  series = {Lecture Notes in Computer Science},
  year = {2005}
}
@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}
}
@INPROCEEDINGS{HWS06,
  author = {M. Huisman and P. Worah and K. Sunesen},
  title = {A temporal logic characterisation of observational determinism},
  topics = {team},
  booktitle = {19th IEEE Computer Security Foundations Workshop},
  publisher = {IEEE Computer Society},
  month = {July},
  year = 2006
}
@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.},
  year = {2006},
  pages = {329-344},
  editor = {J. Domingo-Ferrer and
               J. Posegga and
               D. Schreckling},
  booktitle = {Smart Card Research and Advanced Applications, 7th IFIP
               WG 8.8/11.2 International Conference, CARDIS 2006},
  month = APR,
  publisher = {Springer-Verlag},
  series = {LNCS},
  volume = {3928},
  isbn = {3-540-33311-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@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}
}
@MISC{BBCGHLPR06:FMCO,
  title = { {JACK:}  a tool for validation of security and behaviour of 
Java applications},
  author = {G. Barthe and L. Burdy and J. Charles and B. Gr\'egoire and M. 
Huisman and J.-L. Lanet and M. Pavlova and A. Requet},
  booktitle = {FMCO},
  year = 2006,
  note = {Abstract for tutorial, longer version to appear}
}
@PHDTHESIS{Pavlova:phd,
  title = {Bytecode Verification and its Applications},
  author = {Mariela Pavlova},
  year = {2007},
  month = JAN,
  school = {Universit\'e de Nice Sophia-Antipolis},
  topics = {team}
}
@PHDTHESIS{Dadeau:phd,
  title = {√Čvaluation symbolique √† contraintes pour
la validation, application à Java/JML},
  author = {F. Dadeau},
  year = {2006},
  month = JULY,
  school = {Universit\'e de Franche-Comt\'e},
  topics = {team}
}
@INPROCEEDINGS{bdg07:oip,
  author = {Bouquet, F. and Dadeau, F. and Groslambert, J.},
  title = {{JML2B}: Checking {JML} specifications with {B} machines},
  crossref = {B2007}
}
@INPROCEEDINGS{bdgj06:ip,
  author = {Bouquet, F. and Dadeau, F. and Groslambert, J. and Julliand, J.},
  title = {Safety Property Driven Test Generation from {JML} Specifications},
  booktitle = {FATES/RV'06, 1st Int. Workshop on Formal Approaches to Testing and Runtime Verification},
  pages = {225--239},
  series = {LNCS},
  volume = 4262,
  publisher = {Springer},
  editors = {Havelund, K. and Garcia, M. and Rosu, G. and Wolff, B.},
  address = {Seattle, WA, USA},
  month = AUG,
  year = 2006
}
@INPROCEEDINGS{bdl06:ip,
  author = {Bouquet, F. and Dadeau, F. and Legeard, B.},
  title = {Automated Boundary Test Generation from {JML} Specifications},
  booktitle = {FM'06, 14th Int. Conf. on Formal Methods},
  pages = {428--443},
  series = {LNCS},
  volume = 4085,
  publisher = {Springer-Verlag},
  editors = {Nipkow, T. and Misra, J.},
  address = {Hamilton, Canada},
  month = AUG,
  year = 2006
}
@INPROCEEDINGS{bdl06:onp,
  author = {Bouquet, F. and Dadeau, F. and Legeard, B.},
  title = {{JML-Testing-Tools}, un Animateur Symbolique de Sp\'ecifications {JML}},
  booktitle = {AFADL'06, Approches Formelles dans l'Assistance au D\'eveloppement de Logiciels},
  address = {Paris, France},
  month = MAR,
  year = 2006,
  note = {Session outils}
}
@INPROCEEDINGS{dadeau06:onp,
  author = {Dadeau, F.},
  title = {Animation de mod\`eles {JML} et g\'en\'eration de tests fonctionnels},
  booktitle = {{MAJECSTIC}'06, {MA}nifestation de {JE}unes {C}hercheurs {STIC}},
  address = {Lorient, France},
  month = NOV,
  year = 2006,
  url = {http://web.univ-ubs.fr/lester/www-lester/Evenements/Majecstic/}
}
@INPROCEEDINGS{bdl05:ip,
  author = {Bouquet, F. and Dadeau, F. and Legeard, B.},
  title = {How Symbolic Animation can help designing an Efficient Formal Model},
  booktitle = {Procs of the 7th Int. Conf. on Formal Engineering Methods (ICFEM'05)},
  pages = {96--110},
  volume = 3785,
  series = {LNCS},
  address = {Manchester, UK},
  publisher = {Springer-Verlag},
  editors = {Lau, K.K. and Banach, R.},
  isbn = {3-540-29797-9},
  month = NOV,
  year = 2005
}
@INPROCEEDINGS{bdl05:oip,
  author = {Bouquet, F. and Dadeau, F. and Legeard, B.},
  title = {Using Constraint Logic Programming for the Symbolic Animation of Formal Models},
  booktitle = {Procs of the Int. Workshop on Constraints in Formal Verification (CFV'05) -- Co-located with the Int. Conf. on Automated Deduction (CADE'05)},
  pages = {32--46},
  address = {Tallinn, Estonia},
  editor = {Marques-Silva, J. and Velev, M.},
  month = JUL,
  year = 2005
}
@INPROCEEDINGS{gg06:ip,
  author = {Giorgetti, A. and Groslambert, J.},
  title = {{JAG}: {JML} {A}nnotation {G}eneration for Verifying Temporal 
Properties},
  booktitle = {FASE'2006, Fundamental Approaches to Software Engineering},
  series = {LNCS},
  volume = 3922,
  pages = {373--376},
  address = {Vienna, Austria},
  publisher = {Springer},
  url = {http://dx.doi.org/10.1007/11693017_27},
  month = MAR,
  year = 2006
}
@INPROCEEDINGS{gjk06:ip,
  author = {Groslambert, J. and Julliand, J. and Kouchnarenko , O.},
  title = {{JML}-based Verification of Liveness Properties on a Class},
  booktitle = {SAVCBS'06, Specification and Verification of 
Component-Based Systems },
  editors = {},
  address = {Portland, Oregon, USA},
  month = NOV,
  year = 2006
}
@MASTERSTHESIS{ayache05master,
  author = {Nicolas Ayache},
  title = {Coop\'eration d'outils de preuve interactifs et automatiques},
  school = {Universit{\'e} Paris 7},
  year = 2005,
  topics = {team},
  type_publi = {rapport}
}
@MASTERSTHESIS{lescuyer06master,
  author = {St\'ephane Lescuyer},
  title = {Codage de la logique du premier ordre polymorphe multi-sort\'ee 
dans la logique sans sortes},
  school = {MPRI},
  topics = {team},
  year = 2006
}
@INPROCEEDINGS{contejean05cade,
  author = {Evelyne Contejean and Pierre Corbineau},
  title = {Reflecting Proofs in First-Order Logic with Equality},
  topics = {team},
  pages = {7--22},
  booktitle = {20th International Conference on Automated Deduction (CADE-20)},
  address = {Tallinn, Estonia},
  month = JUL,
  year = 2005,
  series = {LNAI},
  number = 3632,
  publisher = {Springer-Verlag}
}
@INPROCEEDINGS{ConchonFilliatre06wml,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Type-Safe Modular Hash-Consing}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Portland, Oregon},
  month = SEP,
  year = 2006,
  url = {http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.ps.gz}
}
@INPROCEEDINGS{Filliatre06wml,
  author = {Jean-Christophe Filli\^atre},
  title = {{Backtracking iterators}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  address = {Portland, Oregon},
  month = SEP,
  year = 2006,
  url = {http://www.lri.fr/~filliatr/publis/enum2.ps.gz}
}
@INPROCEEDINGS{ConchonFilliatre07jfla,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Union-Find Persistant}},
  year = 2007,
  booktitle = {Dix-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
  note = {to appear},
  month = JAN,
  publisher = {INRIA},
  url = {http://www.lri.fr/~filliatr/ftp/publis/puf.ps.gz}
}
@INPROCEEDINGS{gg06:onp,
  author = {Giorgetti, A. and Groslambert, J.},
  title = {{JAG}~: G\'en\'eration d'annotations {JML} pour v\'erifier des
 propri\'et\'es temporelles},
  booktitle = {AFADL'06, Approches Formelles dans l'Assistance au
 D\'eveloppement de Logiciels},
  address = {Paris, France},
  month = {March},
  year = {2006},
  note = {Session outils},
  url = {http://lifc.univ-fcomte.fr/publis/papers/pub/2006/RT2006-02.pdf}
}
@INPROCEEDINGS{groslambert07:oip,
  author = {Groslambert, J. },
  title = {A {JAG} extension for verifying {LTL} properties on {B} Event Systems},
  crossref = {B2007},
  pages = {262--265}
}
@INPROCEEDINGS{groslambert07:ip,
  author = {Groslambert, J. },
  title = {Verification of {LTL} on {B} Event Systems},
  crossref = {B2007}
}

This file has been generated by bibtex2html 1.85.