Stage PFE – Recherche et intégration d’outils de preuve formelle pour la génération de tests vidéo

Allegro_light1
Our Company

Créée en 2003, Allegro DVT est une entreprise internationale en forte croissance. Son expertise est mondialement reconnue dans le domaine de la vidéo numérique sur le marché des semi-conducteurs. Les équipes sont basées en France, en Chine, aux Etats- Unis et au Royaume-Uni.

Le savoir-faire d’Allegro DVT est notamment présent dans les caméras de voiture, les jeux vidéo, les téléphones portables, les montres connectées, les caméras de surveillance, etc…

Les acteurs majeurs de la micro-électronique, de l’industrie automobile et les acteurs dans le secteur de diffusion et streaming vidéo comptent parmi ses clients. Ses produits sont des leviers d’attractivité pour les marchés émergents tels que l’IA, les véhicules autonomes, la robotique et la santé.

Chez Allegro DVT vous trouverez des projets innovants, variés et passionnants !

CONTEXTE

Les normes d’encodage vidéo sont de plus en plus complexes. Cette complexité nécessite le développement de décodeurs matériels dédiés afin de pouvoir décoder des vidéos en temps réel.

Allegro DVT développe des suites de test (sous forme de flux vidéo compressés) permettant de valider pleinement ce type de décodeur.

De par leur complexité, les codecs vidéo récents nécessitent la mise en place de cas de test très particuliers pouvant faire intervenir différents outils de la norme, dans le cadre de leur validation. Pour construire une suite de tests, nous utilisons notre propre générateur. Pour avoir une suite de tests qualitative, il est nécessaire d’identifier de nouveaux critères et de nouvelles manières de couvrir l’ensemble de la norme.

Notre suite cherche donc à couvrir, certes, les différentes branches de la norme, mais également, par exemple, les valeurs minimales ou maximales de certaines équations.

A mesure que la liste de critères grandit et que les normes se complexifient, il est nécessaire de développer de nouveaux outils et techniques pour améliorer la rapidité et l’efficacité de ce travail.

Job Tasks

Ce stage porte sur un outil de preuve formelle basé sur les solveurs de problème SMT (Satisfiability modulo theories) nommé KLEE. Cet outil permet, entre autres, de rechercher et d’obtenir une suite de valeurs permettant d’atteindre un morceau de code. Cela revient à trouver une entrée à un programme exécutant et donc testant ce morceau de code.

Dans notre contexte de génération de suite de tests, on comprend donc qu’un tel outil pourrait potentiellement être utilisé pour générer automatiquement une suite de tests couvrant de manière basique l’ensemble du code d’un décodeur vidéo, enlevant ainsi une partie du travail humain à réaliser.

Malheureusement, ce genre d’outil est limité par ses performances gourmandes en ressources et son temps d’exécution très long. Une utilisation directe nous est par conséquent interdite.

Ce stage a pour objet d’étudier le domaine de recherche lié à cet outil, et d’évaluer quelles possibilités nous sont offertes. Soit pour optimiser cet outil pour nos besoins, soit pour lui trouver de nouvelles formes d’utilisation dans notre travail.

Profile

Nous recherchons des étudiant(e)s en 3ème année d’école d’ingé- nieurs en informatique ou équivalent.

  • Connaissance du langage de script Bash ;
  • Connaissance des langages C / C++ ;
  • Connaissance de Git et Docker.

Ce projet inclut une part significative de recherche, et un fort esprit d’initiative est attendu !

Une forte appétence pour le domaine de la vidéo numérique ? Nous avons beaucoup à nous apporter mutuellement alors postulez pour nous rejoindre !

INFORMATIONS PRATIQUES

Stage basé à Montbonnot-Saint-Martin (Inovallée) accessible avec le bus C1.

Rémunération : 1.200 € bruts mensuels + chèques déjeuners 9,5 €/jour avec prise en charge de 60% par l’employeur + remboursement 50% des transports en commun.

Send an application for this job