Baptiste Pollien

Baptiste Pollien

PhD Student in Formal Methods

ISAE-SUPAERO

Biography

I am a PhD student at ISAE-SUPAERO, in Toulouse. My thesis deals with formal methods applied on UAV autopilot, especially Paparazzi autopilot developed at ENAC. I am currently working on the verification of the Paparazzi flight plan generator using Coq. I previously worked on the verification of a mathematical library of Paparazzi using Frama-C with EVA and WP plugins. I focused on the verification of the absence of runtime errors (overflows, divisions by 0…) but I also verified some functional properties.

Interests
  • Formal Methods
  • Coq
  • Frama-C
  • Critical Systems
  • UAV Autopilots
Education
  • PhD in Formal Methods, Present

    ISAE-SUPAERO - Toulouse, FRANCE

  • Master’s Degree in Engineering, 2020 - 2017

    ENSIMAG - Grenoble, FRANCE

  • Preparation for entry to engineering schools, 2017 - 2015

    Univ. Grenoble Alpes - Grenoble, FRANCE

Talks

Formal verification of an UAV autopilot
A Verified UAV Flight Plan Generator
Paparazzi UAV Flight Plan Generator Verified in Coq
Paparazzi UAV Flight Plan Generator Verified in Coq
Formal verification of an UAV autopilot

Experience

 
 
 
 
 
Thales
Embedded Software Intern
Mar 2020 – Aug 2020 Grenoble, France
Use of Yocto to generate a specific Linux image for an embedded system used in the industrial field.
 
 
 
 
 
SAP-SE
Software Developer Intern
Jun 2019 – Aug 2019 Walldorf, Germany

Responsibilities include:

  • Development of a drone control application for parking surveillance.
  • Use of Machine Learning for animal detection. Once an animal is detected, it is automatically followed by the drone to scare it away.
 
 
 
 
 
NSIGMA
Web and Mobile Developer
Jun 2018 – Sep 2018 Grenoble, France

Commissioned by the NSIGMA Junior entreprise of ENSIMAG.

  • Developed a mobile application using Ionic framework and integrated MondialRelay (Delivery system) and Mangopay (Payment system) API.
  • Developed a e-commerce website using Prestashop CMS.
 
 
 
 
 
INRIA
Placement in a national research institution
Jun 2017 – Jul 2017 Grenoble, France
In National Institute for Research in Computer Science and Automation, used Coq (a proof assistant) to prove some property about Round-robin process scheduler.
 
 
 
 
 
Squadrone
Customer support & Log analysis Intern
Jul 2016 – Aug 2016 Grenoble, France

Responsibilities include:

  • Respond to customers.
  • Analysed of drone log and decided if a crash was under warranty.
 
 
 
 
 
INRIA
Placement in a national research institution
Jun 2016 – Jul 2016 Grenoble, France
Discovery and handling of Coq, a proof assistant used to certify properties of programming languages and for the formalisation of mathematics.

Teaching

Teaching assistant

2022/2023

2021/2022

  • Languages translation, ENSEEIHT, 1st year graduate
  • Computer Science, ISAE-SUPAERO, 3rd year undergraduate
  • Abstract Types and Advanced Functional Programming, Université Toulouse III - Paul Sabatier, 3rd year undergraduate

2020/2021

  • Computer Science, ISAE-SUPAERO, 3rd year undergraduate
  • Abstract Types and Advanced Functional Programming, Université Toulouse III - Paul Sabatier, 3rd year undergraduate

Accomplish­ments

Tenth Summer School on Formal Techniques
See certificate

Contact