Le LSL étudie les outils d'aide à la validation et à la vérification de logiciels et de systèmes matériels/logiciels (en particulier systems on chip). La validation est la mise en évidence de propriétés particulières et la vérification est la confrontation de propriétés aux systèmes étudiés. Les propriétés peuvent être de diverses natures, par exemple des propriétés

• fonctionnelles : le système remplit la fonction attendue,
• structurelles, par exemple l'absence de code mort, ou encore la couverture des instructions par un ensemble de tests,
• de sûreté, par exemple l'absence d'erreurs à l'exécution comme une division par zéro ou un blocage,
• de performances, par exemple un pire temps d'exécution,
• de précision d'un calcul en nombres flottants

Conformément à sa vocation de transfert technologique, le LSL a développé plusieurs prototypes d'outils capables de traiter des logiciels ou systèmes réels provenant du monde industriel. Des coopérations avec les industriels et les éditeurs d'outils permettent de transformer ces prototypes avancés en outils opérationnels si possible commercialisés.

L'objectif du LSL est d'aider l'industrie à augmenter le niveau d'automatisation de la vérification et validation de ses produits. Ceci afin d'augmenter leur qualité et leur fiabilité et d'en diminuer les temps et les coûts de développement. Dans cet objectif, le LSL a acquis, et continue à développer, la maîtrise de nombreuses techniques parmi les plus avancées dans le domaine

• l'analyse statique à l'aide de la logique de Hoare,
• l'interprétation abstraite,
• les techniques de réécriture de termes et de preuve,
• la simulation généralisée de systèmes logiciel-matériel (analyse dynamique),
• la programmation logique par contraintes,
• l'instrumentation du code source pour recueillir des observations sur l'exécution,
• l'analyse géométrique de la concurrence temporelle.

Ces techniques sont implémentées et mises en oeuvre pour aider à diverses tâches de validation et vérification, dont

• l'aide à la preuve formelle,
• la génération automatique de cas de test basée sur le code source et/ou sur les spécifications,
• l'exécution par simulation de cas de test,
• l'analyse de la précision numérique de calculs sur les nombres flottants et
• la validation de programmes parallèles ou distribués asynchrones.

Les mêmes techniques pouvant être utilisées à des fins différentes, il y a une communication constante et fructueuse entre les équipes travaillant sur les différents thèmes ci-dessous, qui partagent tous comme objectifs :

• de trouver des erreurs,
• de cerner les limites d'utilisation ou
• d'évaluer les performances du logiciel ou système étudié.

Les travaux du laboratoire sont centrés autour des thèmes suivants, qui sont suffisamment ouverts pour être étendus à d'autres applications, même en dehors du domaine de la sûreté

• analyse statique du C
• analyse statique de SystemC
• analyse de la précision numérique
• analyse du parallélisme
• assistance à la préparation du test de logiciel
• simulation généralisée logiciel-matériel et environnement de test

Un thème regroupe en moyenne 3 à 4 permanents, plus des doctorants et stagiaires. Certains thèmes plus exploratoires peuvent regrouper moins de personnes, d'autres en général plus avancés peuvent avoir un effectif plus important du fait de partenariats industriels.