pub2009.bib

@ARTICLE{roegel:2006:inria-00111244:1,
  author = {Roegel, Denis},
  title = {Prototype Fragments from Babbage's First Difference Engine},
  journal = {IEEE Annals of the History of Computing},
  publisher = {IEEE},
  volume = {31},
  number = {2},
  pages = {70-75},
  year = {2009},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  url-hal = {http://hal.inria.fr/inria-00111244/en},
  x-id-hal = {inria-00111244}
}
@ARTICLE{roegel:2008:inria-00337215:1,
  author = {Roegel, Denis},
  title = {An introduction to nomography: Garrigues' nomogram for the computation of Easter},
  journal = {Tugboat},
  publisher = {TeX Users Group},
  volume = {30},
  number = {1},
  pages = {88-104},
  year = {2009},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  url-hal = {http://hal.inria.fr/inria-00337215/en},
  x-id-hal = {inria-00337215}
}
@ARTICLE{mery:2009:inria-00426383:1,
  author = {M\'ery, Dominique},
  title = {Refinement-Based Guidelines for Algorithmic Systems},
  journal = {International Journal of Software and Informatics},
  publisher = {Institute of Software, Chinese Academy of Sciences},
  volume = {3},
  number = {2-3},
  pages = {197-239},
  year = {2009},
  month = SEP,
  url = {http://www.ijsi.org/IJSI/ch/reader/view{\_}abstract.aspx?file{\_}no=197{\&}flag=1},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  url-hal = {http://hal.inria.fr/inria-00426383/en},
  x-id-hal = {inria-00426383}
}
@ARTICLE{mery:2009:inria-00426384:1,
  author = {Méry, Dominique},
  doi = {10.1145/1595453.1595462},
  title = {A Simple Refinement-based Method for Constructing Algorithms},
  journal = {ACM SIGCSE Bulletin},
  publisher = {ACM},
  volume = {41},
  number = {2},
  pages = {51-59},
  year = {2009},
  month = JUN,
  x-international-audience = {yes},
  x-editorial-board = {yes},
  url-hal = {http://hal.inria.fr/inria-00426384/en},
  x-id-hal = {inria-00426384}
}
@ARTICLE{cansell:2009:inria-00426385:1,
  author = {Cansell, Dominique and Méry, Dominique and Proch, Cyril},
  doi = {10.1007/s10009-009-0104-7},
  title = {System-on-chip design by proof-based refinement},
  journal = {International Journal on Software Tools for Technology Transfer (STTT)},
  publisher = {Springer Berlin / Heidelberg},
  volume = {11},
  number = {3},
  pages = {217-238},
  year = {2009},
  month = MAR,
  x-international-audience = {yes},
  x-editorial-board = {yes},
  url-hal = {http://hal.inria.fr/inria-00426385/en},
  x-id-hal = {inria-00426385}
}
@ARTICLE{charronbost:2009:inria-00426388:1,
  author = {Charron-Bost, Bernadette and Merz, Stephan},
  title = {Formal Verification of a Consensus Algorithm in the Heard-Of Model},
  journal = {International Journal of Software and Informatics},
  publisher = {Science Press (Beijing, China)},
  volume = {3},
  number = {2-3},
  pages = {273-303},
  year = {2009},
  url = {http://www.ijsi.org/IJSI/ch/reader/view{\_}abstract.aspx?file{\_}no=273{\&}flag=1},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  url-hal = {http://hal.inria.fr/inria-00426388/en},
  x-id-hal = {inria-00426388}
}
@ARTICLE{caminhabdeoliveira:2009:inria-00430636:1,
  author = {Caminha B. De Oliveira, Diego and Déharbe, David and Fontaine, Pascal},
  x-pays = {BR},
  doi = {10.1016/j.entcs.2009.05.048},
  title = {Combining Decision Procedures by (Model-)Equality Propagation},
  journal = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier},
  volume = {240},
  number = {2},
  pages = {113-128},
  year = {2009},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  url-hal = {http://hal.inria.fr/inria-00430636/en},
  x-id-hal = {inria-00430636}
}
@ARTICLE{roegel:2009:inria-00432213:1,
  author = {Roegel, Denis},
  title = {MetaPost macros for drawing Chinese and Japanese abaci},
  journal = {Tugboat},
  publisher = {TUG},
  volume = {30},
  number = {1},
  pages = {74-79},
  year = {2009},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  url-hal = {http://hal.inria.fr/inria-00432213/en},
  x-id-hal = {inria-00432213}
}
@ARTICLE{roegel:2009:inria-00432214:1,
  author = {Roegel, Denis},
  title = {Spheres, great circles and parallels},
  journal = {Tugboat},
  publisher = {TUG},
  volume = {30},
  number = {1},
  pages = {80-87},
  year = {2009},
  x-international-audience = {yes},
  x-editorial-board = {yes},
  url-hal = {http://hal.inria.fr/inria-00432214/en},
  x-id-hal = {inria-00432214}
}
@ARTICLE{fass:2009:inria-00437320:1,
  author = {Fass, Didier},
  title = {Design et ingénierie des systèmes homme-dans-la boucle},
  journal = {La revue des Ingénieurs},
  publisher = {InterMines},
  number = {440},
  pages = {50-51},
  year = {2009},
  month = MAY,
  x-editorial-board = {yes/no},
  x-international-audience = {no},
  x-scientific-popularization = {yes},
  url-hal = {http://hal.inria.fr/inria-00437320/en},
  x-id-hal = {inria-00437320}
}
@INPROCEEDINGS{fass:2009:hal-00394608:1,
  author = {Fass, Didier and Lieber, Romain},
  title = {Rationale for human modelling in human in the loop systems design},
  booktitle = {3rd Annual IEEE International Systems Conference, SysCon 2009},
  year = {2009},
  month = MAR,
  publisher = {IEEE},
  pages = {27-30},
  note = {ISBN : 978-1-4244-3463-3},
  address = {Canada Vancouver},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url-hal = {http://hal.inria.fr/hal-00394608/en},
  x-id-hal = {hal-00394608}
}
@INPROCEEDINGS{chaouchsaad:2009:inria-00408908:1,
  author = {Chaouch-Saad, Mouna and Charron-Bost, Bernadette and Merz, Stephan},
  doi = {10.1007/978-3-642-04420-5{\_}10},
  title = {A Reduction Theorem for the Verification of Round-Based Distributed Algorithms},
  booktitle = {Reachability Problems 2009},
  year = {2009},
  series = {Lecture Notes in Computer Science},
  editor = {Olivier Bournez and Igor Potapov},
  publisher = {Springer Berlin / Heidelberg},
  volume = {5797},
  pages = {93-106},
  address = {France Palaiseau},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url-hal = {http://hal.inria.fr/inria-00408908/en},
  x-id-hal = {inria-00408908}
}
@INPROCEEDINGS{schimpf:2009:inria-00408950:1,
  author = {Schimpf, Alexander and Merz, Stephan and Smaus, Jan-Georg},
  doi = {10.1007/978-3-642-03359-9{\_}29},
  title = {Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL},
  booktitle = {22nd International Conference Theorem Proving in Higher-Order Logics - TPHOLs 2009},
  year = {2009},
  series = {Lecture Notes in Computer Science},
  editor = {Tobias Nipkow and Christian Urban},
  publisher = {Springer Berlin / Heidelberg},
  volume = {5674},
  pages = {424-439},
  address = {Germany Munich},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url-hal = {http://hal.inria.fr/inria-00408950/en},
  x-id-hal = {inria-00408950}
}
@INPROCEEDINGS{benaissa:2009:inria-00426405:1,
  author = {Benaissa, Nazim and Méry, Dominique},
  title = {Développement combiné et prouvé de systèmes transactionnels cryptologiques},
  booktitle = {Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL 2009},
  year = {2009},
  month = JAN,
  address = {France Toulouse},
  x-international-audience = {no},
  x-proceedings = {yes},
  url-hal = {http://hal.inria.fr/inria-00426405/en},
  x-id-hal = {inria-00426405}
}
@INPROCEEDINGS{fontaine:2009:inria-00430631:1,
  author = {Fontaine, Pascal},
  doi = {10.1007/978-3-642-04222-5{\_}16},
  title = {Combinations of theories for decidable fragments of first-order logic},
  booktitle = {7th International Symposium, FroCoS 2009},
  year = {2009},
  series = {Lecture Notes in Computer Science},
  editor = {Silvio Ghilardi and Roberto Sebastiani},
  publisher = {Springer Verlag},
  volume = {5749},
  pages = {263-278},
  note = {The original publication is available at www.springerlink.com},
  address = {Italy Trento},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url-hal = {http://hal.inria.fr/inria-00430631/en},
  x-id-hal = {inria-00430631}
}
@INPROCEEDINGS{bouton:2009:inria-00430634:1,
  author = {Bouton, Thomas and Caminha B. De Oliveira, Diego and Déharbe, David and Fontaine, Pascal},
  x-pays = {BR},
  doi = {10.1007/978-3-642-02959-2{\_}12},
  title = {veriT: an open, trustable and efficient SMT-solver},
  booktitle = {22nd International Conference on Automated Deduction - CADE 22},
  year = {2009},
  series = {Lecture Notes in Computer Science},
  editor = {Renate A. Schmidt},
  publisher = {Springer Berlin / Heidelberg},
  volume = {5663},
  pages = {151-156},
  note = {The original publication is available at www.springerlink.com},
  address = {Canada Montreal},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url-hal = {http://hal.inria.fr/inria-00430634/en},
  x-id-hal = {inria-00430634}
}
@INPROCEEDINGS{deharbe:2009:inria-00430637:1,
  author = {Déharbe, David and Fontaine, Pascal and Martins Moreira, Anamaria and Merz, Stephan and Santana De Oliveira, Anderson},
  x-pays = {BR},
  title = {Automating model-based software engineering},
  booktitle = {Colloque d'Informatique: Brésil/INRIA (COLIBRI)},
  year = {2009},
  pages = {22-27},
  address = {Brazil Bento Gon{\c{c}}alves},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url-hal = {http://hal.inria.fr/inria-00430637/en},
  x-id-hal = {inria-00430637}
}
@INPROCEEDINGS{benaissa:2009:inria-00431253:1,
  author = {Benaissa, Nazim and Méry, Dominique},
  title = {Cryptologic protocols analysis using proof-based patterns},
  booktitle = {Seventh International Andrei Ershov Memorial Conference «PERSPECTIVES OF SYSTEM INFORMATICS» - PSI 2009},
  year = {2009},
  month = JUN,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  address = {Russian Federation Novosibirsk},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url-hal = {http://hal.inria.fr/inria-00431253/en},
  x-id-hal = {inria-00431253}
}
@INPROCEEDINGS{benaissa:2009:inria-00431264:1,
  author = {Benaissa, Nazim and Méry, Dominique},
  title = {Cryptographic Protocols Analysis in Event B},
  booktitle = {Seventh International Andrei Ershov Memorial Conference «PERSPECTIVES OF SYSTEM INFORMATICS» - PSI 2009},
  year = {2009},
  month = NOV,
  series = {Lectures Notes in Computer Science},
  publisher = {Springer-Verlag},
  address = {Russian Federation Novosibisrk},
  x-international-audience = {yes},
  x-proceedings = {yes},
  url-hal = {http://hal.inria.fr/inria-00431264/en},
  x-id-hal = {inria-00431264}
}
@INPROCEEDINGS{tounsi:2009:hal-00361933:1,
  author = {Tounsi, Mohamed and Hadj Kacem, Ahmed and Mosbah, Mohamed and Méry, Dominique},
  title = {A Refinement Approach for Proving Distributed Algorithms : Examples of Spanning Tree Problems},
  year = {2009},
  month = FEB,
  booktitle = {Integration of Model-based Formal Methods and Tools - IM{\_}FMT'2009 - in IFM'2009},
  address = {Germany Düsseldorf},
  x-international-audience = {yes/no},
  x-proceedings = {no},
  url-hal = {http://hal.inria.fr/hal-00361933/en},
  x-id-hal = {hal-00361933}
}
@INPROCEEDINGS{rehm:2009:inria-00362715:1,
  author = {Rehm, Joris},
  title = {Pattern Based Integration of Time applied to the 2-Slots Simpson Algorithm},
  year = {2009},
  booktitle = {Integration of Model-based Formal Methods and Tools - IM{\_}FMT'2009 - in IFM'2009},
  address = {Germany Düsseldorf},
  x-international-audience = {yes},
  x-proceedings = {no},
  url-hal = {http://hal.inria.fr/inria-00362715/en},
  x-id-hal = {inria-00362715}
}
@INPROCEEDINGS{rosa:2010:inria-00378374:2,
  author = {Rosa, Cristian and Quinson, Martin and Merz, Stephan},
  title = {Model-checking Distributed Applications with GRAS},
  year = {2009},
  booktitle = {Exploiting Concurrency Efficiently and Correctly - EC2 workshop associated to CAV 2009},
  address = {France Grenoble},
  x-international-audience = {yes},
  x-proceedings = {no},
  url-hal = {http://hal.inria.fr/inria-00378374/en},
  x-id-hal = {inria-00378374}
}
@INPROCEEDINGS{lopezfraguas:2009:inria-00408964:1,
  author = {López Fraguas, Francisco and Merz, Stephan and Rodríguez Hortalá, Juan},
  x-pays = {ES},
  title = {A Formalization of the Semantics of Functional-Logic Programming in Isabelle},
  year = {2009},
  booktitle = {22nd International Conference on Theorem Proving in Higher-Order Logics : emerging trends session - TPHOLs 2009},
  organization = {Technische Universität München},
  address = {Germany Munich},
  x-international-audience = {yes},
  x-proceedings = {no},
  url-hal = {http://hal.inria.fr/inria-00408964/en},
  x-id-hal = {inria-00408964}
}
@INPROCEEDINGS{rehm:2009:inria-00431246:1,
  author = {Rehm, Joris},
  title = {A Rodin plugin for quantitative timed models},
  year = {2009},
  month = JUL,
  editor = {Michael Butler and Stefan Hallerstede and Laurent Voisin},
  booktitle = {Rodin User and Developer Workshop},
  address = {United Kingdom Southampton},
  x-international-audience = {yes},
  x-proceedings = {no},
  url-hal = {http://hal.inria.fr/inria-00431246/en},
  x-id-hal = {inria-00431246}
}
@TECHREPORT{mery:2009:inria-00419973:2,
  author = {Méry, Dominique and Singh, Neeraj Kumar},
  title = {Pacemaker's Functional Behaviors in Event-B},
  type = {Research Report},
  year = {2009},
  url-hal = {http://hal.inria.fr/inria-00419973/en},
  x-id-hal = {inria-00419973}
}
@TECHREPORT{rosa:2009:inria-00422159:1,
  author = {Rosa, Cristian and Quinson, Martin and Merz, Stephan},
  title = {Model-checking Distributed Applications with GRAS},
  type = {Research Report},
  pages = {11},
  year = {2009},
  institution = {INRIA},
  number = {RR-7052},
  url-hal = {http://hal.inria.fr/inria-00422159/en},
  x-id-hal = {inria-00422159}
}
@TECHREPORT{siebert:2010:inria-00435569:3,
  author = {Siebert, Julien and Rehm, Joris and Chevrier, Vincent and Ciarletta, Laurent and Méry, Dominique},
  title = {AA4MM coordination model and event-B specification},
  type = {Research Report},
  pages = {22},
  year = {2009},
  institution = {INRIA},
  number = {RR-7081},
  url-hal = {http://hal.inria.fr/inria-00435569/en},
  x-id-hal = {inria-00435569}
}
@PHDTHESIS{rehm:2009:tel-00441312:1,
  author = {Rehm, Joris},
  title = {Gestion du temps par le raffinement},
  year = {2009},
  month = DEC,
  school = {Universit\'e Henri Poincar\'e - Nancy I},
  url-hal = {http://hal.inria.fr/tel-00441312/en},
  x-id-hal = {tel-00441312}
}

This file has been generated by bibtex2html 1.87.