Explore les concepts d'ingénierie logicielle, en soulignant l'importance des tests et des spécifications claires pour assurer l'exactitude du logiciel.
Introduit la vérification formelle et ses avantages par rapport aux méthodes de test traditionnelles, en discutant de la démonstration automatique des théorèmes et en compilant les déclarations d'exactitude dans des conditions de vérification.
Se concentre sur l'utilisation d'Inox pour la vérification des programmes, en démontrant le processus de vérification des programmes et en assurant l'exactitude.
Examine les défis et les avantages de la vérification des compilateurs, en soulignant l'importance de la vérification des compilateurs pour les logiciels critiques.
Introduit Stainless, un outil open-source pour vérifier les programmes Scala, couvrant le langage, la modélisation, les conseils de vérification et les travaux intérieurs.
Explore le flou, les oracles de bogues, les revues de codes et les techniques de test automatisé, soulignant l'importance de la désinfection pour détecter les défauts.
Explore les logiciels validés pour la validation continue du système dans des environnements critiques pour la sécurité, en soulignant l'importance de l'assurance en temps réel anticipée et de la validation au niveau sémantique.
Couvre la conception, la mise en œuvre et la vérification formelle des systèmes distribués, en se concentrant sur les systèmes et organisations distribués vérifiables.
Explore la vérification des modèles de détermination du temps, la planification U-Pool, l'analyse des pires temps d'exécution et la vérification statistique des modèles pour les systèmes cyber-physiques.
Couvre la programmation assistée par solveur, intégrant les résolveurs SMT pour la vérification, la synthèse et le débogage des programmes, ainsi que les défis dans la construction d'outils assistés par solveur.
Explore la programmation fonctionnelle vérifiée, la vérification formelle, les résolveurs SMT, la vérification de type, les fonctionnalités Scala, l'automatisation et les types dépendants.
Couvre la génération de code pour un compilateur, traduisant un programme Amy à WebAssembly, y compris la gestion de la mémoire et la compilation de correspondance de motifs.
