Prédicats de représentation pour la vérification déductive

Frama-C est une plateforme collaborative pour l'analyse de programmes écrits en C. Parmi les outils proposés au sein de Frama-C, WP est dédié à la vérification déductive de programme, qui permet la preuve mathématique de propriétés fonctionnelles et l'absence d'erreurs à l'exécution. Cet outil est utilisé depuis des années dans l'industrie.
La logique de séparation est la voie la plus prometteuse pour permettre la preuve de propriétés sur des programmes manipulant des structures de données complexes. Cependant, il est difficile de l'utiliser pour des études de cas industrielles. La principale raison à cela est la difficulté pour l'encoder vers des outils de preuve automatique. Aussi, son utilisation nécessite beaucoup de travail de la part de l'utilisateur.
L'outil WP de Frama-C n'utilise pas la logique de séparation. Un projet de recherche actuel vise à intégrer certains éléments de logique de séparation pour augmenter les performances et les capacité de WP à traiter des structures complexes. Cependant, l'extension proposée ne permet pas de traiter des structures récursives, pour cela les prédicats de représentation de la logique de séparation doivent être ajoutés. Le but de ce postdoc est d'étudier l'intégration de ces prédicats à WP.

Exploitation des méthodes formelles pour la gestion des interférences au sein des systèmes embarqués H/F

Au sein d’une équipe de recherche technologique pluridisciplinaire d’experts en outils de co-design SW/HW par application de méthodes formelles, vous intervenez dans un projet national de recherche visant à développer un environnement pour identifier, analyser et réduire les interférences engendrées par l’exécution concurrente d’applicatifs sur une plateforme matérielle multi-coeur hétérogène sur étagère (COTS)

Top