Menu

David BRAUN

STRASBOURG

En résumé

Docteur en informatique de l'Université de Strasbourg, spécialisé en certification du logiciel et en imagerie, à la recherche d'un défi scientifique et technologique innovant répondant aux enjeux de demain.

J'ai effectué mon doctorat dans l'équipe IGG de l'ICube depuis le 1 septembre 2015 jusqu'au 31 octobre 2019 en travaillant sous la direction de Pascal Schreck. Je suis également encadré par Nicolas Magaud. Mon sujet de thèse s'intitule : "Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective".

Mes compétences :
CoQ
LaTeX
Maple
Shaders
Python
HTML 5
CSS 3
Java
C/C++
OpenGL
OCaml
PL/SQL

Entreprises

  • ICube - Stagiaire en recherche

    2015 - 2015 Stage de recherche au sein du laboratoire ICube dans l'équipe Informatique Géométrique et Graphique (IGG). Sujet : approche combinatoire pour l'automatisation en Coq de démonstrations formelles en géométrie projective.

    Research Internship in the laboratory ICube in Computer Graphics team (IGG). Subject : combinatorial approach for automation in Coq formal demonstrations in projective geometry.

    Encadrants - Tutors : Nicolas Magaud & Pascal Schreck

  • ICube - Ingénieur Logiciel

    2014 - 2014 Projet de développement au sein du laboratoire Icube dans l'équipe Informatique Géométrique et Graphique (IGG). Sujet : vérification automatique de l'encyclopédie de Kimberling sur les centres des triangles.

    Internship in the laboratory ICube in Computer Graphics team (IGG). Designing a vector graphics using Bezier curves. Subject : Automatic verification of the Kimberling's encyclopedia on the centers of triangles.

    Website : http://dpt-info.u-strasbg.fr/~narboux/CETC/about.html

    Encadrant - Tutor : Julien Narboux

  • ICube - Stagiaire : Ingénieur Logiciel

    2014 - 2014 Stage au sein du laboratoire ICube dans l'équipe Modèles, Images et Vision (MIV) sur le projet TrADiCont. Conception d'un logiciel sur la manipulation des Ω-AQAs. Ce travail a donné lieu à la publication d'un article présenté à Reims Image 2014 : Les Ω-AQA : représentation discrète des applications affines.

    Internship in the laboratory ICube in Models, Image and Vision team (MIV) on TrADiCont project. Designing a software for handling Ω - AQAs . This work resulted in the publication of a paper presented at Reims Image 2014 : Les Ω-AQA : représentation discrète des applications affines.

    Encadrants - Tutors : Loïc Mazo, Marie-Andrée Da Col & Nicolas Magaud

  • ICube - Ingénieur Logiciel

    2014 - 2014 Travaux d'études et de recherche dans l'équipe Informatique Géométrique et Graphique (IGG). Formalisation de théorème en géométrie à l'aide de l'assistant de preuve Coq.

    Research project in Computer Graphics team (IGG). Formalization of theorem in geometry using the Coq proof assistant.

    Website : http://ddbraun.free.fr/Thales/

    Encadrant - Tutor : Nicolas Magaud

  • ICube - Stagiaire : Ingénieur Logiciel

    2013 - 2013 Stage au sein du laboratoire ICube dans l'équipe Informatique Géométrique et Graphique (IGG). Conception d'un logiciel de dessin vectoriel utilisant courbes de Beziers.

    Internship in the laboratory ICube in Computer Graphics team (IGG). Designing a vector graphics using Bezier curves.

    Encadrant - Tutor : Sylvain Thery

Formations

  • Icube

    Strasbourg 2015 - 2019 Doctorat

    Titre : Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective

    Title : Combinatorial approach for automation in Coq of formal proofs in incidence projective geometry

    Jury composé de - Jury composed of :
    - Jacques Fleuriot, Professeur des Universités - Université d'Edimbourg (rapporteur)
    - Dominique Michelucci, Professeur des Universités - Uni

  • Université De Strasbourg

    Strasbourg 2013 - 2015 Master

    Mention Bien

    Informatique :

    Compilation - Algorithmique avancé - Algorithmique distribué - Complexité et calculabilité - Conception et programmation objet avancée - Logiciels et matériels graphiques - Fondements et algorithmiques de l'imagerie numérique - Ingénierie de la preuve - Traitements de l'image - Conception assisté par ordinateur - Sémantique - Banque de données multimédias - Certificat

  • Université De Strasbourg

    Strasbourg 2009 - 2013 Licence

    Mention Bien

    Informatique :

    Algèbre - Analyse - Probabilité,statistique et combinatoire - Algorithmique - Structure de Données - Pratique et Fondements des systèmes d'exploitation - Programmation Fonctionnelle - Technique de développement - Théorie des graphes - Théorie des langages - Logique et programmation logique - Base de données - Architecture des ordinateurs - Génie Logiciel - Programmat

  • Lycée De Bouxwiller

    Bouxwiller 2006 - 2009 Baccalauréat

    Mention Bien

Réseau

Annuaire des membres :