Recherche

Accueil CEDRIC > Publications > Article > Liste >

Liste des publications

2017

Conférence Internationale avec comité de lecture

[CT17] P. Courtieu, S. Tixeuil. "Certified Gathering of Oblivious Mobile Robots: Survey of Recent Results and Open Problems", FMICS-AVoCS 2017, September 2017, Vol. 10471, pp.165-181, Series LNCS, Turin, Italy, (DOI: 10.1007/978-3-319-67113-0_11)

2016

Conférence Internationale avec comité de lecture

[CUT16a] P. Courtieu, X. Urbain, S. Tixeuil, L. Rieg. "Certified Universal Gathering in {\textbackslash}mathbb {R} {\^{}}2 for Oblivious Mobile Robots", DISC 2016, Distributed Computing 30th International Symposium, September 2016, Vol. 9888, pp.187-200, Series LNCS, Paris, France, (DOI: 10.1007/978-3-662-53426-7_14)
[CUT16] P. Courtieu, X. Urbain, S. Tixeuil, L. Rieg. "Brief Announcement: Certified Universal Gathering in R2 for Oblivious Mobile Robots", PODC '16: Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing, July 2016, pp.439-441, Chicago, US, (DOI: 10.1145/2933057.2933070)

Conférences Internationales sans actes

[CP16] P. Courtieu, C. Pit-Claudel. "Company-Coq: Taking Proof General one step closer to a real IDE", CoqPL'16: International Workshop on Coq for Programming Languages, St Petersburgh, United-States, Florida,

2015

Atelier, Poster ou Démonstration dans une Conférence Internationale

[PDL15] T. Pham , C. Dubois, N. Levy. "Towards correct-by-construction product variants of a software product line: GFML, a formal language for feature modules", Formal Methods and Analysis in SPL Engineering (FMSPLE 2015), April 2015, Vol. 182, pp.44-55, London, UK, (DOI: 10.4204/EPTCS.182)

2014

Conférence Internationale avec comité de lecture

[ABR14] M. Abbas, C. Ben Yelles, R. Rioboo. "Modeling UML Template Classes with FoCaLiZe", Integrated Formal Methods, September 2014, pp.87--102, Series LNCS,
[DDM14] D. Delahaye, C. Dubois, C. MarchÃ©, D. MentrÃ©. "The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations", Abstract State Machines, Alloy, B, VDM, and Z (ABZ), June 2014, pp.-,

Rapport Scientifique

[CRT14] P. Courtieu, L. Rieg, S. Tixeuil, X. Urbain. "Impossibility of Gathering, a Certification", Date de dépot: 2014/05/22, Nb pages 10, (Tech. Rep.: CEDRIC-14-3016)

2013

Conférence Internationale avec comité de lecture

[DDG13] D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, O. Hermant. "Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo", Logic for Programming Artificial Intelligence and Reasoning (LPAR), December 2013, Vol. 8312, pp.274-290, Series LNCS/ARCoSS, Stellenbosch, South Africa,
[DDG13a] D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, O. Hermant. "Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps", International Workshop on the Implementation of Logics, December 2013, pp.-,

Conférences invitées

[Del13] D. Delahaye. "Automated Deduction Modulo", Proof-Search in Axiomatic Theories and Type Theories (PSATTT), November 2013, pp.online, Palaiseau, France,

Conférences Internationales sans actes

[Bur13] G. Burel. "A Shallow Embedding of Resolution and Superposition Proofs into the Î»Î -Calculus Modulo", Third International Workshop on Proof Exchange for Theorem Proving, Lake Placid, USA,

Mémoire de Thèse

[Tol13] P. Tollitte. "Extraction de code fonctionnel certifiÃ© Ã partir de spÃ©cifications inductives", Soutenue le: 06 December 2013, pp. 180,

2012

Conférence Internationale avec comité de lecture

[CAM12] P. Courtieu, M. Aponte, Y. Moy, M. Sango. "Maximal and Compositional Pattern-Based Loop Invariants", Formal method 2012 (FME), August 2012, Vol. 7436, pp.37-51, Series LNCS, Paris, France,
[JBD12] M. Jacquel, K. Berkani, D. Delahaye, C. Dubois. "Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover", International Joint Conference on Automated Reasoning (IJCAR 2012), June 2012, Vol. 7364, pp.332--338, Series LNAI, Manchester, UK,

Conférences Internationales sans actes

[BB12] M. Boespflug, G. Burel. "CoqInE : Translating the calculus of inductive constructions into the Î»Î -calculus modulo.", Second International Workshop on Proof Exchange for Theorem Proving (PXTP 2012), Manchester, United Kingdom,

2011

Revue Internationale avec comité de lecture

[Bur11] G. Burel. "Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo", Logical Methods in Computer Science, vol. 7(3:1), pp. 1-31, 2011, (doi:10.2168/LMCS-7(1:3)2011)

Conférence Internationale avec comité de lecture

[CCF11a] E. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain. "Automated Certified Proofs with CiME 3", 22nd Int. Conf. on Rewriting Techniques and Applications, May 2011, Vol. 10, pp.21-30, Series LIPIcs, Novi Sad, Serbie,

Conférences Internationales sans actes

[Bur11a] G. Burel. "Consistency Implies Cut Admissibility", International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Wroclaw, Poland,

Rapport Scientifique

[CCF11] E. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain. "Automated Certified Proofs with CiME3", Date de dépot: 2011/02/01, Nb pages 11, (Tech. Rep.: CEDRIC-11-2044)

2010

Mémoire de HDR

[Urb10] X. Urbain. "Preuve automatique : techniques, outils et certification", Soutenue le: 29 November 2010, pp. 77,

2008

Rapport Scientifique

[CFU08a] E. Contejean, J. Forest, X. Urbain. "Deep-Embedded Unification", Date de dépot: 2008/01/01, (Tech. Rep.: CEDRIC-08-1547)

2007

Rapport Scientifique

[CCF07] E. Contejean, P. Courtieu, J. Forest, O. Pons, X. Urbain. "Certification of automated termination proofs", Date de dépot: 2007/01/01, (Tech. Rep.: CEDRIC-07-1185)