Inférence de synchronisation

Cette séance de cours couvre la synthèse automatique de la synchronisation correcte et efficace dans les programmes, en se concentrant sur l'objectif de générer des programmes synchronisés à partir d'un point de départ intuitif. Le processus consiste à supprimer l'atomicité redondante, à réorganiser les instructions et à ajouter des métadonnées de synchronisation. La séance de cours explore également les défis de la réduction de l'atomique, de l'application des transformations et du processus de vérification de la génération. En outre, il se décline en ensembles simultanés, les étapes de génération et de vérification de la synchronisation, et le concept de synthèse guidée par abstraction pour la vérification automatique. La séance de cours se termine par une discussion sur le projet IBM Paraglide et les implications de la synthèse guidée par l'abstraction dans la vérification des programmes.