Qed at Large: A Survey of Engineering of Formally Verified Software
Le développement de preuves formelles de l'exactitude des programmes peut accroître la fiabilité réelle et perçue et faciliter une meilleure compréhension des spécifications des programmes et de leurs hypothèses sous-jacentes. Les outils permettant ce développement sont disponibles depuis plus de 40 ans, mais n'ont été que récemment largement utilisés dans la pratique.
Les projets basés sur la construction de preuves formelles vérifiées par machine atteignent aujourd'hui une échelle sans précédent, comparable à celle des grands projets logiciels, ce qui entraîne de nouveaux défis en matière de développement et de maintenance des preuves. Malgré son importance croissante, le domaine de l'ingénierie de la preuve est rarement considéré en tant que tel ; les théories, les techniques et les outils qui s'y rapportent couvrent de nombreux domaines et lieux. QED at Large couvre la chronologie et la littérature de recherche concernant le développement de preuves pour la vérification de programmes, y compris les théories, les langages et les outils.
Elle met l'accent sur les défis et les percées à chaque étape de l'histoire et souligne les défis actuels en raison de l'ampleur croissante des développements de preuves. Cette monographie est destinée aux chercheurs et aux étudiants qui découvrent le domaine.
Elle fournit au lecteur un aperçu perspicace des travaux qui ont conduit aux techniques modernes de vérification formelle des logiciels. À une époque d'automatisation croissante, ces techniques sont à la base de nombreux systèmes logiciels, de sorte que les tendances futures sont également mises en évidence.
© Book1 Group - tous droits réservés.
Le contenu de ce site ne peut être copié ou utilisé, en tout ou en partie, sans l'autorisation écrite du propriétaire.
Dernière modification: 2024.11.14 07:32 (GMT)