monkey king Olivier Ly
Associate Professor
Bordeaux 1 university - IUT A

LaBRI - Université BORDEAUX 1
351, cours de la Libération

33405 Talence CEDEX - FRANCE

LaBRI: Office 275  /  phone: (+33).  /  fax: +

[ research - publications ]

Research Interests Team: Formal Methods and Rhoban - LaBRI

I have created and I lead the Rhoban Project. The Rhoban Team won the RoboCup Kid-Size League in 2016 and 2017. We also got the Best Humnoid Robot Price 2017.
I have been one of founding member of the FFROB, and I am the chair of the French Regional RoboCup Committee.

• Twitter @rhobanrobots : please visit

• Facebook : rhobanmetabot

Past and Present Projects:
  • RHOBAN Project [ Humanoid and Autonomous Robotics ]
I have been a member of the Inria team (2010-2012) FLOWERS [ Developmental and Social Robotics ]

  • D. Bitonneau (in collaboration with B. Claverie)
Past Students:

Habilitation à Diriger des Recherche: Un parcours de recherche des méthodes formelles aux robots humanoïdes.

Doctorat: Etude Algorithmique de Complexes Simpliciaux Infinis. PhD Thesis - Bordeaux 1 University (2000). [supervisors: G. Sénizergues & Ph. Narbel]

Agrégation de Mathématiques (1995).
red wooman (Nicolas Ly - 1999)


With Hugo Gimbert, I have created and I lead the Rhoban project which deals with humanoid and autonomous robotics. The project is transversal and regroups several researchers and students from different areas of the LaBRI. People from academic world but not only actually.

Until now, we designed small autonomous humanoid robots. Small robots actually because this makes experiments easier, in particular when dealing with learning algorithms, which need experiments. (see here).

Rhoban takes part to the RoboCup competition. The largest competition of robotics and artificial intelligence in the world. Our team participates to the soccer league of the competition, which is the root of the competition. The principle is simple: make a team of autonomous humanoid robots play soccer...
The origin of the challenge is to explore motricity and artificial intelligence in a framework of
partial information about the state of the game
collaboration and distributed strategy between the agents (the players of the team)
simulaneous and parallel operations of all the agents (players and opponents)
Let us note also that the context of competition, even if it is before all a research community, requires high operating safety level.

Rhoban won the RoboCup Kid-Size League in 2016 and 2017. We are also very proud of the RoboCup Best Humnoid Robot Price 2017. Please have a look! I have been one of founding member of the FFROB, and I am the chair of the French Regional RoboCup Committee.

I am deeply involved on the RoboCup Bordeaux 2020 application. We want to welcome the
competition (3500 competitors, 450 teams, 45 nations, 30 000m2) in Bordeaux in 2020.

The projet deals also with agricultural robotics (see Autoplan project for Alliance Forêt-Bois or AgroGeoVisio with Razol company, or in wineyard in collaboration with Pépinières Duvigneau).

We now collaborate with several companies: R&Drone, Vitirover, Alliance Forêts-Bois, Razol, Génération Robot, Safran / Herakles, IdeoFluid, Proteor.

The Rhoban project started years ago by designing from scratch a small ludic humanoid robot called Rhoban able to walk, get up, go upstairs ... and even dance ! Look at him here. I thus carried on by designing the Acroban humanoid robot, supported by the LaBRI, in collaboration with the Inria Flowers project. In 2012, we showed ours robots at the international expo in Korea (8 millions visitors). Look at the robots here :).

Humanoid Robot RhoBan

Software Security

Nicolas Ly - 1998
My work regarding software security concerns smart card technology. I am interested in particular in these aspects of security:

Verification of Security Properties using Formal Methods

In collaboration with J. Andronick  (LRI - AXALTO) and B. Chetali  (AXALTO), I investigate the use of the Coq proof assistant for the formal verification of applet isolation properties in Java Card technology. We focus on the confidentiality property. Our work aims at showing how this property is verified by the embedded Java Card virtual machine card manager and the APIs. We also aim at setting up a verification method which allows to complete specifications and to enhance the secure design of the platform. For instance, we describe how the proof of the integrity puts the light on a known bug. Some
more information about this work can be found in this paper.

Software Counter-Measures against Physical Attacks of Smart Cards

I have been the main architect of the CFED project (Control Flow Error Detection - AXALTO copyright).
This work is developed in collaboration with Louis Goubin from AXALTO company. AXALTO (formerly Schlumberger Systems) is
the smart card and terminal division of Schlumberger Limited.

This technology aims at enforcing semi-automatically counter-measures against fault injection attacks of smart cards. It addresses in a generic way the whole software embedded on the card. In particular, it addresses threats going beyond cryptography-related parts of the embedded software, like threats against the firewall of the Java Card embedded virtual machine, the PIN code verification, etc. Counter-measures are automatically integrated to the source code during the pre-compilation step, according to a guideline defined by the programmer under the form of a set of directives included into the source code. All this technology is developed with  the OCAML language. 

Some more information about this work can be found in this paper; this technology is protected by a patent belonging to AXALTO company.

Infinite Model Theory

My recent work in this area concerns the problem of compositionality of specifications of sequential programs.
This consists in deciding in an effective way whether or not a given set of local structural properties of the functions of a program implies a given global behavioural property of the program.
I focus on properties expressed in monadic second-order logic dealing with the control flow of the program and the function calls occuring during its execution. This problem has been investigated in relation with the security of open multi-application smart cards.
I proved that the compositionality is a decidable problem for sequential programs whose control-flow graphs are of tree-width less than a fixed integer value, which includes in particular structured programs.

More information about this work can be found in this paper.
people (Nicolas Ly - 1998)


Design of an industrial humanrobot system through participative simulations - Tank cleaning case study.
Bitonneau D., Moulieres-Seban T., Dumora J., Ly O., Thibault J.-F., Salotti J.-M., Claverie B.
In proc. of IEEE/SICE Int. Symp. on System Integration. SII 2017: 1-8

Rhoban Football Club: RoboCup Humanoid Kid-Size 2016 Champion Team Paper.
Allali, J. and Deguillaume, L. and Fabre, R. and Gondry, L. and Hofer, L. and Ly, O. and NGuyen, S. and Passault, G. and Pirrone, A. and Rouxel, Q.
In proc. of RoboCup 2016: Robot Soccer World Cup Symposium 2016. Lecture Notes in Artificial Intelligence (LNAI).

Optimizing Morphology and Locomotion On a Corpus of Parametric Legged Robots.
Passault, G. and Rouxel, Q. and Fabre, R. and NGuyen, S. and Ly, O.
Proc. of Biomimetic and Biohybrid Systems: 5th International Conference, Living Machines 2016, Edinburgh, Scotland, 2016.

Dynaban, an Open-Source Alternative Firmware for Dynamixel Servo-Motors.
R. Fabre, Q. Rouxel, G. Passault, S. N'Guyen, O. Ly.
In proc. of RoboCup Symposium 2016. Lecture Notes in Artificial Intelligence (LNAI).

Learning the odometry on a small humanoid robot.
Q. Rouxel, G. Passault, L. Hofer, S. N'Guyen, and O. Ly.
In proc. IEEE International Conference on Robotics and Automation (ICRA 2016).

Metabot: low-cost legged robotics platform for education.
G. Passault, Q. Rouxel and O. Ly.
In proc. of IEEE International Conference on Autonomous Robot Systems and Competitions (ICARSC'2016). 2016

Low-cost force sensors for small size humanoid robot.
G. Passault, Q. Rouxel, L. Hofer, S. N'Guyen, O. Ly.
In proc. of 15th IEEE-RAS Int. conf. on Humanoids Robots (Humanoids'2015). Interactive session. Seoul. 2015.

A Fully Autonomous Robot for Putting Posts for Trellising Vineyard with Centimetric Accuracy.
O. Ly, H. Gimbert, G. Passault, and G. Baron.
In proc. of IEEE International Conference on Autonomous Robot Systems and Competitions (ICARSC'2015). 2015. (Vila Real).

Rhoban Hardware and Software Open Source Contributions for RoboCup Humanoids.
Rouxel, Q. and Passault, G. and Hofer, L. and NGuyen, S. and Ly, O.
In Proc of 10th Workshop on Humanoid Soccer Robots. IEEE-RAS Int. Conference on Humanoid Robots, Seoul, Korea. 2015.

On effective construction of the greatest solution of language inequality XA ⊆ BX.
with Zhilin Wu
Theor. Comput. Sci. 528: 12-31 (2014)

An experiment of low cost entertainment robotics.
with Paul Fudal, Hugo Gimbert, Loic Gondry, Ludovic Hofer, Gregoire Passault.
RO-MAN 2013: 820-825

Exploring robust, intuitive and emergent physical human-robot interaction with the humanoid robot Acroban
with Pierre-Yves Oudeyer and Pierre Rouanet.
In 11th IEEE-RAS International Conference on Humanoid Robots (Humanoid'2011) - 2011 (Bled)

Maturational constraints for motor learning in high-dimensions: the case of biped walking
with Matthieu Lapeyre and Pierre-Yves Oudeyer.
In 11th IEEE-RAS International Conference on Humanoid Robots (Humanoid'2011) - 2011 (Bled)

Bio-Inspired Vertebral Column, Compliance and Semi-Passive Dynamics in a Lightweight Humanoid Robot
with Matthieu Lapeyre and Pierre-Yves Oudeyer
In proc. of IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'2011) - 2011 (San Francisco)
(also selected for IROS'2011 Special Demonstration Symposium)

Modeling Maturational Constrains for Learning Biped Humanoid Locomotion
with Matthieu Lapeyre and Pierre-Yves Oudeyer
In Proc of Int. Conf. on Development and Learning (ICDL) - Poster session - IEEE 2011 (Frankfurt)

Automated Extraction of Polymorphic Virus Signatures using Abstract Interpretation
with Renaud Tabary and Serge Chaumette
In proc. of 5th Int. Conf. on Network and System Security (NSS'2011) - IEEE - 2011 (Milan) 

The BINCOA Framework for Binary Code Analysis
with Sebastien Bardin, Philippe Herrmann, Jérôme Leroux, Aymeric Vincent and Renaud Tabary
In proc. of 23rd Int. Conf. on Computer Aided Verification (CAV'2011) - 2011 (SnowBird, Utah)

Modeling Long Term Signature Validation for Resolution of Dispute.
with M. Ben MBarka and F. Krief
In proc. of Theory of Security and Applications, TOSCA'2011 (ETAPS joint event) 2011. LNCS

Automated Software Protection through Program Externalization on Memory-Limited Secure Devices.
with S. Chaumette and R. Tabary.
In proc. of IEEE
Int. Symp. on Trusted Computing and Communication (TRUSTCOM'10) (Hong Kong).

Acroban the Humanoid: Compliance for Stabilization and Human Interaction.
with P.-Y. Oudeyer.
In IEEE/RSJ Int. Conference on Intelligent Robots and Systems (IROS'2010) – Video Session (Taipei 2010).

Acroban the Humanoid: Playful and Compliant Physical Child-Robot Interaction.
with P.-Y. Oudeyer.
In ACM SIGGRAPH'2010 Emerging Technologies (Los Angeles 2010)

Entrusting Remote Software Executed in an Untrusted Computation Helper
with F. Krief and M. Ben MBarka
In proceedings of Network and Service Security (N2S'2009), Paris (2009)

A smartcard power analysis simulator
with P. Andouard and C. Thuillet
In proceedings of IEEE Int. Symp. on Trusted Computing and Communication,
(TRUSTCOM'09) Vancouver.

Context-free Categorical Grammars
with Michel Bauderon and Rui Chen
In proceedings of "3rd International  Conference on Algebraic Informatics" (CAI'09), Thessaloniki (2009).

Sûreté de fonctionnement et sécurité des algorithmes cryptographiques
with Louis Goubin.
Multi-system & Internet Security Cookbook (MISC) no 42 (2009).

Pullback Grammars are Context-Free
with Michel Bauderon and Rui Chen
proceedings of "4th International Conference on Graph Transformation" (ICGT'08), Leicaster (2008).
LNCS 5214, p366-378. Springer, December 2008.

VisAA: Visual Analyzer for Assembler
with Philippe Andouard, Davy Rouillard
In proc. of "Int. Conf. on Risks and Security of Internet and Systems"
(CRISIS'08), IEEE, Tozeur (2008)

A constructive solution of the language inequation XA ⊆ BX

proceedings of  "Theory and Applications of Language Equations", Turku.
General Publications series
of Turku Centre for Computer Science, 44 p 76-84 (2007). [pdf]

Distance Labeling in Hyperbolic Graphs
with Cyril Gavoille
proceedings of "16th Annual International Symposium on Algorithms and Computation" Sanya China
(ISAAC'05) LNCS 3827, p1071-1081, December 2005. [pdf]

Compositional Verification: Decidability Issues Using Graph Substitutions
proceedings of  "29th Mathematical Foundations of Computer Science", Prague
(MFCS'2004) LNCS 3153, p 537-549 (2004). [pdf]

Automatic Graph and D0L-Sequences of Finite Graphs
Journal of Computer and System Sciences - JCSS 67:3, p 497-545
(2003). [pdf]

Construction of Pseudo-Isometries for Tree-Like Non-Compact 3-Manifolds
Comptes Rendus de l'Académie des Sciences - CRAS 337:7, p 457-460

Using Coq to Verify Java Card Applet Isolation Properties
with J. Andronick and B. Chetali
proceedings of "16th Theorem Proving in Higher Order Logic", Roma
(TPHOL'2003) LNCS 2758
, p335-351 (2003).

Automatic Graph and Graph D0L-Systems
proceedings of  "25th Mathematical Foundations of Computer Science", Bratislava
(MFCS'2000) LNCS 1893, p 539-548 (2000).

The Weak Monadic Quantifier Alternation Hierarchy of Equationnal Graphs is Infinite
proceedings of "20th Foundations of Software Technology and Theoretical Computer Science", New Delhi
(FST-TCS'2000) LNCS 1974; p188-200 (2000).

On Effective Decidability of the Homeomorphism Problem for Non-Compact Surfaces
Contemporary Mathematics 250, p89-112. AMS (1998).


Procédé de sécurisation d'un dispositif électronique exécutant un algorithme quelconque
contre les attaques
par introduction d'erreur.
O.Ly, M.-L. Akkar and L. Goubin
International Patent EP1460546 A1 ; US Patent 2010 n°7774653
5 (Schlumberger, 2003)

Articulation de membre inférieur pour la locomotion bipède.
O. Ly, H. Gimbert, G. Passault, Q. Rouxel.
Brevet National 2016- n° de pub.: WO2016189253 A1 - En cours d'internationalisation.

Dispositif de guidage d'un attelage entrainé par un véhicule, et procédé correspondant.
H. Gimbert, O. Ly, G. Passault, P. Lezer.
Brevet National 2016 - n° de pub.: WO2016128688 A1


Bio-inspired vertebral column, compliance and semi-passive dynamics in a lightweight humanoid robot
with P.-Y. Oudeyer
LaBRI/INRIA 2011 [pdf]

Automated Signature Extraction for Precise Detection of Polymorphic Self-Replicating Malwares
with R. Tabary and S. Chaumette
LaBRI (2011) [pdf]

A Note about Compositional Verification of Sequential Programs.
(2004) [pdf]

Automatic Integration of Counter-Measures against Fault Injection Attacks.
with M.-L. Akkar and L. Goubin
(2003) [pdf]

Classification des surfaces non-compactes planaires à bord
LaBRI (1998)

Selected Conferences and Talks


The ACROBAN Platform
3rd french/german workshop on Humanoid and Legged Robots (HLR'2011) Paris.


Formal Verification of the Integrity Property in Java Card Technology
with J. Andronick and B. Chetali
E-SMART - Nice 2003

About an Automatic Fault Injection Protection System
M.-L. Akkar and L. Goubin
E-SMART - Nice 2003

An Interpretation of the Common Criteria EAL 7 Level:
Formal Modelling of the JavaCard Virtual Machine.
with B. Chetali, E. Giménéz and C. Loiseaux
International Common Criteria Conference (ICCC'2002) - Otawa 2002.

Formal Verification of the Confidentiality Property in Java Card Technology
with B. Chetali
- Nice 2002

Formal Modelling and Verification of the JavaCard Security Architecture:
From Static Checkings to Embedded Applet Execution
with E. Giménéz
VERIFICARD annual meeting - Marseilles 2002.

last update: march 2011