Programmation assistée par solvant pour tous

Cette séance de cours présente Solver-Aided Programming, un modèle intégrant les solveurs SMT dans le langage pour fournir des constructions pour la vérification, la synthèse et le débogage des programmes. Il couvre des sujets tels que la programmation avec des outils assistés par un solveur, la localisation de mauvaises parties d'un programme, la recherche de valeurs pour réparer les pannes et la synthèse du code. La séance de cours aborde également les défis de la construction d'outils assistés par un solveur et présente ROSETTE, un langage assisté par un solveur. Il explore l'espace de conception des langues spécifiques au domaine, l'anatomie des langues d'accueil assistées par solveur et la traduction des programmes aux contraintes. En outre, il se transforme en fusion d'état de type, des applications assistées par solveur dans divers domaines, et des stratégies pour les jeux et l'éducation. La séance de cours se termine par un accent mis sur la vérification des logiciels de systèmes, y compris la vérification des composants du système d'exploitation et l'utilisation des vérificateurs de Serval.