Pierre Courtieu
Pierre Courtieu
Conservatoire des Arts et Métiers - Laboratory: CÉDRIC
Verified email at cnam.fr
TitleCited byYear
Certification of automated termination proofs
E Contejean, P Courtieu, J Forest, O Pons, X Urbain
International Symposium on Frontiers of Combining Systems, 148-162, 2007
662007
Automated certified proofs with CiME3
E Contejean, P Courtieu, J Forest, O Pons, X Urbain
22nd International Conference on Rewriting Techniques and Applications (RTA'11), 2011
442011
Certified impossibility results for byzantine-tolerant mobile robots
C Auger, Z Bouzid, P Courtieu, S Tixeuil, X Urbain
Symposium on Self-Stabilizing Systems, 178-190, 2013
402013
Efficient reasoning about executable specifications in Coq
G Barthe, P Courtieu
International Conference on Theorem Proving in Higher Order Logics, 31-46, 2002
402002
A3PAT, an approach for certified automated termination proofs
É Contejean, A Paskevich, X Urbain, P Courtieu, O Pons, J Forest
Proceedings of the 2010 ACM SIGPLAN workshop on Partial evaluation and …, 2010
382010
Impossibility of gathering, a certification
P Courtieu, L Rieg, S Tixeuil, X Urbain
Information Processing Letters 115 (3), 447-452, 2015
312015
Tool-assisted specification and verification of the JavaCard platform
G Barthe, P Courtieu, G Dufay, SM de Sousa
International Conference on Algebraic Methodology and Software Technology, 41-59, 2002
282002
Certified Universal Gathering in for Oblivious Mobile Robots
P Courtieu, L Rieg, S Tixeuil, X Urbain
International Symposium on Distributed Computing, 187-200, 2016
252016
Normalized types
P Courtieu
International Workshop on Computer Science Logic, 554-569, 2001
252001
Improved matrix interpretation
P Courtieu, G Gbedo, O Pons
International Conference on Current Trends in Theory and Practice of …, 2010
192010
Certifying a termination criterion based on graphs, without graphs
P Courtieu, J Forest, X Urbain
International Conference on Theorem Proving in Higher Order Logics, 183-198, 2008
152008
Company-Coq: Taking Proof General one step closer to a real IDE
C Pit-Claudel, P Courtieu
142016
Structural analysis of narratives with the Coq proof assistant
AG Bosser, P Courtieu, J Forest, M Cavazza
International Conference on Interactive Theorem Proving, 55-70, 2011
142011
A certified universal gathering algorithm for oblivious mobile robots
P Courtieu, L Rieg, S Tixeuil, X Urbain
arXiv preprint arXiv:1506.01603, 2015
112015
Hardening large-scale networks security through a meta-policy framework
M Blanc, P Clemente, P Courtieu, S Franche, L Oudot, C Toinard, ...
Third Workshop on the Internet, Telecommunications and Signal Processing, 2004
112004
CiME3, 2004
E Contejean, C Marché, X Urbain
11
Formal methods for mobile robots: current results and open problems
B Bérard, P Courtieu, L Millet, M Potop-Butucaru, L Rieg, N Sznajder, ...
International Journal of Informatics Society 7 (3), 101-114, 2015
72015
A novel approach for distributed updates of MAC policies using a meta-protection framework
M Blanc, P Courtieu, G Hains, L Oudot, C Toinard
Proceedings of the 15th IEEE International Symposium on Software Reliability …, 2004
72004
Certified Gathering of Oblivious Mobile Robots: survey of recent results and open problems
T Balabonski, P Courtieu, L Rieg, S Tixeuil, X Urbain
Critical Systems: Formal Methods and Automated Verification, 165-181, 2017
52017
Maximal and compositional pattern-based loop invariants
V Aponte, P Courtieu, Y Moy, M Sango
International Symposium on Formal Methods, 37-51, 2012
52012
The system can't perform the operation now. Try again later.
Articles 1–20