courtieu-bib2.bib
@techreport{balabonski18rrasync,
title = {{\textbf{Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots}}},
author = {Balabonski, Thibaut and Courtieu, Pierre and Pelle, Robin and Rieg, Lionel and Tixeuil, S{\'e}bastien and Urbain, Xavier},
url = {https://hal.sorbonne-universite.fr/hal-01762962},
type = {Research Report},
pages = {1-12},
institution = {{Sorbonne Universit{\'e}, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, F-75005 Paris, France}},
year = {2018},
pdf = {https://hal.sorbonne-universite.fr/hal-01762962/file/main_tr.pdf},
hal_id = {hal-01762962},
hal_version = {v1}
}
@inproceedings{balabonski18sssba,
author = {Thibaut Balabonski and
Pierre Courtieu and
Robin Pelle and
Lionel Rieg and
S{\'{e}}bastien Tixeuil and
Xavier Urbain},
title = {{\textbf{Brief Announcement: Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots}}},
editor = {Taisuke Izumi and Petr Kuznetsov},
booktitle = {Stabilization, Safety, and Security of Distributed Systems - 20th
International Symposium, (SSS 2018)},
series = {Lecture Notes in Computer Science},
volume = {11201},
year = {2018},
address = {Tokyo, Japan},
publisher = {Springer-Verlag},
month = nov
}
@inproceedings{balabonski17avocs,
author = {Thibaut Balabonski and
Pierre Courtieu and
Lionel Rieg and
S{\'{e}}bastien Tixeuil and
Xavier Urbain},
title = {\textbf{Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems}},
editor = {Laure Petrucci and
Cristina Seceleanu and
Ana Cavalcanti},
booktitle = {Critical Systems: Formal Methods and Automated
Verification - Joint 22nd International Workshop on
Formal Methods for Industrial Critical Systems - and
- 17th International Workshop on Automated
Verification of Critical Systems, (FMICS-AVoCS 2017)},
month = sep,
address = {Turin, Italy},
series = {Lecture Notes in Computer Science},
volume = {10471},
publisher = {Springer-Verlag},
year = {2017},
pages = {165--181},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{courtieupodc16,
author = {Pierre Courtieu and Lionel Rieg and S{\'{e}}bastien Tixeuil and Xavier Urbain},
title = {\textbf{Brief Announcement: Certified Universal Gathering in R\({}^{\mbox{2}}\) for Oblivious Mobile Robots}},
booktitle = {Proceedings of the 2016 {ACM} Symposium on Principles of Distributed Computing, {PODC} 2016, Chicago, IL, USA, July 25-28, 2016},
pages = {439--441},
year = {2016},
doi = {10.1145/2933057.2933070},
pdf = {papers/podc-2016-gathering.pdf}
}
@inproceedings{courtieudisc16,
author = {Pierre Courtieu and Lionel Rieg and S{\'{e}}bastien Tixeuil and Xavier Urbain},
title = {\textbf{Certified Universal Gathering in {\textbackslash}mathbb {R} {\^{}}2 for Oblivious Mobile Robots}},
booktitle = {Distributed Computing - 30th International Symposium, {DISC} 2016, Paris, France, September 27-29, 2016. Proceedings},
pages = {187--200},
year = {2016},
url = {http://dx.doi.org/10.1007/978-3-662-53426-7_14},
doi = {10.1007/978-3-662-53426-7_14},
timestamp = {Mon, 05 Sep 2016 12:49:45 +0200},
pdf = {papers/disc2016-gathering.pdf}
}
@article{courtieu15corr,
author = {Pierre Courtieu and
Lionel Rieg and
S\'ebastien Tixeuil and Xavier Urbain},
title = {{\textbf{A Certified Universal Gathering Algorithm for Oblivious Mobile Robots}}},
journal = {CoRR},
year = {2015},
volume = {abs/1506.01603},
ee = {http://arxiv.org/abs/1506.01603}
}
@article{courtieu15ipl,
author = {Pierre Courtieu and Lionel Rieg and S\'ebastien Tixeuil and Xavier Urbain},
title = {\textbf{Impossibility of Gathering, a Certification}},
journal = {Information Processing Letters},
year = 2015,
volume = {115},
pages = {447-452},
abstract = {This paper builds upon a previously proposed formal
framework to certify the correctness of
impossibility results regarding distributed
algorithms that are dedicated to autonomous mobile
robots evolving in a continuous space. As a case
study, we consider the problem of gathering all
robots at a particular location, not known
beforehand. },
keywords = {mobile robots, swarm, theorem proving, distributed algorithms},
doi = {10.1016/j.ipl.2014.11.001},
pdf = {papers/ipl-2014-impossibility.pdf}
}
@article{berard:hal-01238784,
title = {\textbf{[Invited Paper] Formal Methods for Mobile Robots: Current Results and Open Problems}},
author = {B{\'e}rard, B{\'e}atrice and Courtieu, Pierre and Millet, Laure and Potop-Butucaru, Maria and Rieg, Lionel and Sznajder, Nathalie and Tixeuil, S{\'e}bastien and Urbain, Xavier},
url = {http://hal.upmc.fr/hal-01238784},
journal = {{International Journal of Informatics Society}},
publisher = {{Japan Informatics Society}},
volume = {7},
number = {3},
pages = {101-114},
year = {2015},
hal_id = {hal-01238784},
hal_version = {v1}
}
@inproceedings{courtieuhilt2013,
title = {\textbf{Towards The Formalization of SPARK 2014 Semantics With Explicit Run-time Checks Using Coq }},
year = {2013},
author = {Pierre Courtieu and Maria Virginia Aponte and Tristan Crolard
and Roby, Jason Belt and John Hatcliff and Zhi Zhang
and Jerome Guitton and Trevor Jennings},
optkey = {},
booktitle = {High Integrity Language Technology ACM SIGAda's Annual International Conference (HILT 2013)},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
month = nov,
organization = {ACM},
optpublisher = {},
optnote = {To appear. Extended abstract. 2 pages.},
optannote = {}
}
@inproceedings{augersss2013,
author = { C\'edric Auger and Zohir Bouzid and Pierre Courtieu
and S\'ebastien Tixeuil and Xavier Urbain},
title = {\textbf{Certified Impossibility Results for Byzantine-Tolerant Mobile Robots}},
editor = {Teruo Higashino et al.},
booktitle = {15th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2013)},
series = {Lecture Notes in Computer Science},
year = 2013,
month = nov,
volume = 8255,
note = {To appear. 15 pages}
}
@inproceedings{invariants2012,
title = {\textbf{Maximal and Compositional Pattern-Based Loop Invariants}},
author = { P. Courtieu and M. Aponte and Y. Moy and M. Sango },
booktitle = {Formal method 2012 (FME)},
year = {2012},
month = aug,
series = {lncs},
volume = {7436},
pages = {37-51},
address = {Paris, France},
pdf = {papers/aponte-courtieu-moy-sango-fm2012.pdf}
}
@inproceedings{tatouage2012,
author = {David Baelde and
Pierre Courtieu and
David Gross-Amblard and
Christine Paulin},
title = {\textbf{Towards Provably Robust Watermarking}},
booktitle = {ITP},
year = {2012},
pdf = {papers/watermarking-ITP2012.pdf}
}
@inproceedings{DBLP:conf/itp/BosserCFC11,
author = {Anne-Gwenn Bosser and
Pierre Courtieu and
Julien Forest and
Marc Cavazza},
title = {\textbf{Structural Analysis of Narratives with the Coq Proof Assistant}},
booktitle = {ITP 2011},
series = {LNCS},
volume = {6898},
year = {2011},
pages = {55-70},
ee = {http://dx.doi.org/10.1007/978-3-642-22863-6_7},
bibsource = {DBLP, http://dblp.uni-trier.de},
pdf = {papers/ITP2011_Coq_Emma.pdf}
}
@inproceedings{DBLP:conf/rta/ContejeanCFPU11,
author = {Evelyne Contejean and
Pierre Courtieu and
Julien Forest and
Olivier Pons and
Xavier Urbain},
title = {\textbf{Automated Certified Proofs with CiME3}},
booktitle = {RTA},
year = {2011},
pages = {21-30},
ee = {http://dx.doi.org/10.4230/LIPIcs.RTA.2011.21},
bibsource = {DBLP, http://dblp.uni-trier.de},
pdf = {papers/contejean11rta.pdf}
}
@inproceedings{courtieu10pepm,
author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest,
Andrei Paskevich, Olivier Pons et Xavier Urbain},
title = {\textbf{A3PAT, an Approach for Certified Automated Termination Proofs}},
booktitle = {In PEPM'10 Proceedings of the 2010 ACM SIGPLAN Symp.
on Partial Evaluation and Program Manipulation},
year = {2010},
pdf = {papers/pepm10-contejean.pdf}
}
@inproceedings{courtieu10sofsem,
author = {Pierre Courtieu and
Gladys Gbedo and
Olivier Pons},
title = {\textbf{Improved Matrix Interpretation}},
year = {2010},
pages = {283-295},
ee = {http://dx.doi.org/10.1007/978-3-642-11266-9_24},
bibsource = {DBLP, http://dblp.uni-trier.de},
editor = {Jan van Leeuwen et al. },
booktitle = {In proc. SOFSEM2010, SOFSEM'10, International Conference on Current Trends in Theory and Practice of Computer Science, volume of LNCS},
publisher = {Springer},
pdf = {papers/sofsem-courtieu-gbedo-pons.pdf}
}
@inproceedings{courtieu08tphols,
author = {Pierre Courtieu and Julien Forest and Xavier Urbain},
title = {\textbf{Certifying a {T}ermination {C}riterion {B}ased on {G}raphs, {W}ithout {G}raphs}},
year = {2008},
booktitle = {21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs'08)},
editor = {C\'esar Mu{\~n}oz and Otmane {Ait Mohamed}},
series = {Lecture Notes in Computer Science},
volume = {5170},
pages = {183-198},
address = {Montr\'eal, Canada},
month = aug,
publisher = {Springer-Verlag},
pdf = {papers/tphol08.pdf}
}
@inproceedings{contejean07frocos,
author = {{\'E}velyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
title = {\textbf{Certification of automated termination proofs}},
booktitle = {6th International Symposium on Frontiers of Combining Systems (FroCos 07)},
year = 2007,
editor = {Boris Konev and Frank Wolter},
volume = 4720,
pages = {148--162},
series = {Lecture Notes in Artificial Intelligence},
address = {Liverpool,UK},
month = sep,
publisher = {Springer-Verlag},
pdf = {papers/frocos07.pdf}
}
@inproceedings{blanc+CFIP05,
author = {M. Blanc and P. Clemente and P. Courtieu and S. Franche and L. Oudot and C. Toinard and L. Vessiller},
title = {{\textbf{Am\'elioration de la s\'ecurit\'e des grands r\'eseaux par une infrastructure de m\'eta-politique}}},
booktitle = {CFIP 05},
year = {2005}
}
@inproceedings{blanc+distrmeta,
author = {Mathieu Blanc and Patrice Clemente and Pierre Courtieu
and Stephane Franche and Laurent Oudot and Christian
Toinard and Lionel
Vessiller},
title = {\textbf{Hardening large-scale networks security through a meta-policy framework}},
booktitle = {Third Workshop on the Internet, Telecommunications and
Signal Processing {(WITSP.04)}},
year = {2004},
month = {dec},
address = {Adelaide, Australia},
pdf = {papers/WITSP04.pdf}
}
@inproceedings{blanc+04macmeta,
author = {Mathieu Blanc and Pierre Courtieu and Gaetan Hains and
Laurent Oudot and Christian Toinard},
title = {{\textbf{A novel approach for distributed updates of {MAC} policies using a meta-protection framework}}},
booktitle = {Supplementary Proceedings of the 15th IEEE
International Symposium on Software Reliability Engineering {(ISSRE
2004)}},
year = {2004},
month = {nov},
address = {Saint Malo, France},
pdf = {papers/bcht-ISSRE04.pdf}
}
@article{g+05jak:jar,
author = {G. Barthe and P. Courtieu and G. Dufay and S. Melo de Sousa},
title = {\textbf{Jakarta: tool-assisted specification and verification of the JavaCard Platform}},
month = {October},
volume = {Volume 35, Numbers 1-3},
year = {2005},
pages = {295-354},
journal = {{Journal of Automated Reasoning}},
pdf = {papers/jarck13-v2.pdf}
}
@inproceedings{gp02:tphols,
author = {G. Barthe and P. Courtieu},
title = {{\textbf{Efficient Reasoning about Executable Specifications in Coq}}},
booktitle = {Proceedings of TPHOLs'02},
editor = {V. A Carreno, C. Mu\~noz and S. Tahar},
series = {Lecture Notes in Computer Science},
pages = {{31--46}},
year = {2002},
publisher = {springer},
volume = {2410},
pdf = {papers/barthe-courtieu-tphol2002.pdf}
}
@inproceedings{ggsp02:amast,
author = {G. Barthe and G.~Dufay and Simao de~Sousa and P. Courtieu},
title = {{\textbf{Tool-Assisted Specification and Verification of the JavaCard Platform}}},
booktitle = {Proceedings of AMAST'02},
series = {Lecture Notes in Computer Science},
year = {2002},
pages = {41--59},
publisher = {Springer-Verlag},
volume = {2422},
ps = {papers/bcds-amast02.ps.gz}
}
@inproceedings{courtieulcs01,
author = {Pierre Courtieu},
title = {\textbf{Normalized types}},
booktitle = {Proceedings of CSL2001},
series = {Lecture Notes in Computer Science},
year = 2001,
volume = 2142,
ps = {papers/courtieucsl2001.ps.gz}
}
@inproceedings{courtieufmppta02,
author = {Pierre Courtieu},
title = {\textbf{Proving self-stabilization with a proof assistant}},
booktitle = {Proceedings of IPDPS'2002},
series = {IEEE CS Press},
year = {2002},
note = {contained in IPDPS collected proceedings CD-ROM, Abstract
appears in IPDPS'02 Proc. : Abstracts, p.0209 },
ps = {papers/selfstab-in-coq.ps.gz}
}
@phdthesis{courtieuphd01,
author = {Pierre Courtieu},
title = {{\textbf{Repr{\'e}sentation de structures non libres en th{\'e}orie des types}}},
address = {{Laboratoire de Recherche en informatique}},
year = {2001},
type = {Th{\`e}se de doctorat},
month = {d{\'e}cembre},
type_publi = {these},
topics = {team, lri},
school = {{Universit{\'e} Paris-sud}},
ps = {papers/courtieu-phd.ps.gz},
pdf = {papers/courtieu-phd.pdf},
note = {In french}
}