Raisonnement du programme d'aide à l'apprentissage

Cette séance de cours de l'instructeur couvre les défis fondamentaux dans le raisonnement du programme, comme la recherche de bugs et la vérification, en utilisant des exemples comme le bug Heartbleed. Il explore l'utilisation d'outils d'analyse statique comme Clang Static Analyzer et l'application du raisonnement bayésien différentiel pour prioriser les vraies alarmes sur les fausses alarmes. La séance de cours se penche également sur les défis de l'automatisation et de l'exactitude dans la vérification des programmes, mettant en évidence les contributions de la recherche en tirant parti de l'apprentissage automatique. L'exposé décrit les différents cadres de raisonnement bayésiens et les cadres d'apprentissage de renforcement profond pour la vérification des programmes, en soulignant l'importance des approches axées sur l'apprentissage pour relever ces défis.