Notice bibliographique
Résumé
The importance of verification for software products is being increasingly appreciated in industry, although still not as much as necessary to become a standard development approach for industrial-scale high-quality software.In 2005, a global initiative was started by eminent researchers in both industry and academia, with the aim of establishing and disseminating a culture of software verification from the first principles by means of theories, tools and experiments.This special issue contains a selection of contributions originally presented at the 2008 Workshop on Tools at VSTTE 2008, the conference on Verified Software: Theories, Tools and Experiments in Toronto.The VSTTE series of conferences and workshops focuses on the challenge of verifying software systems.Within VSTTE, the scope of the Tools workshop includes implementations and enabling techniques for program verifiers, which are important ingredients for the dissemination of principles and techniques among industrial practitioners.This special issue complements a sister special issue of the Journal on Software Tools For Technology Transfer (STTT) [STT10].The FAC papers address the foundational aspects of tool-based verification, whereas the STTT selection focuses on practical aspects.The general public perceives the quality of software products as a major issue.In fact, the cost of software construction is dominated by the process of debugging it and validating that the software meets the desired requirements.Due to the prohibitive cost of manual inspection, it is widely believed that computers themselves need to be part of the solution.To this end, Tony Hoare's Grand Challenge for computing research proposes the Verifying Compiler, that is, computer-implemented algorithms that validate the correctness of a given program [Hoa03].In the Manifesto of the Grand Challenge, presented at VSTTE 2005 [MW08, Coo07], the first in the series of VSTTE conferences and workshops, Tony Hoare and Jay Misra directly recognise and appraise the importance of tools as vehicles for the transmission of knowledge to practitioners.In the second paragraph of the introduction, they write: "This paper argues that the time is ripe to embark on an international Grand Challenge project to construct a program verifier that would use logical proof to give an automatic check of the correctness of programs submitted to it.Prototypes for the program verifier will be based on a sound and complete theory of programming; they will be supported by a range of program construction and analysis tools; and the entire toolset will be evaluated and evolve by experimental application to a large and widely representative sample of useful computer programs.The project will provide the scientific basis of a solution for many of the problems of programming error that afflict all builders and users of software today."The paper also suggested that the achievement of this vision should be accelerated by a major international research initiative, modelled on a Grand Challenge, with specific measurable goals.The suggested measure was one million lines of verified code, together with its specifications, designs, assertions, and other artifacts.
Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.
Comment cette classification a été obtenuedéplier
Prédiction machine sur la base complète
Imitation des enseignantsNi prévalence calibrée, ni vérité terrain. Validation humaine à venir. Le volet Gemma est une étiquette directe du modèle pour chaque travail de la base, lue sur la notice réduite au titre. Le volet Codex est un classifieur appris des 10 348 étiquettes directes de Codex et calibré sur les taux pondérés de l'échantillon; les champs sans appui suffisant ne portent aucun appel Codex. Le mode candidate est l'union des deux volets; le consensus est leur intersection. Ces sorties portent le statut machine_predicted_unvalidated et ne sont pas des étiquettes humaines.
Scores du classifieur distillé par catégorie (deux têtes)
| Catégorie | Codex | Gemma |
|---|---|---|
| Métarecherche | 0,003 | 0,016 |
| Méta-épidémiologie (sens strict) | 0,002 | 0,001 |
| Méta-épidémiologie (sens large) | 0,002 | 0,001 |
| Bibliométrie | 0,002 | 0,001 |
| Études des sciences et des technologies | 0,002 | 0,001 |
| Communication savante | 0,006 | 0,004 |
| Science ouverte | 0,002 | 0,001 |
| Intégrité de la recherche | 0,006 | 0,009 |
| Charge utile insuffisante (le modèle a refusé de juger) | 0,046 | 0,040 |
Scores machine (provisoires)
Les deux têtes enseignantes du modèle étudiant, lues sur ce travail. Un score ordonne la base pour la relecture; il n'affirme jamais une catégorie, et le statut de validation accompagne chaque rangée tel quel.
Scores de référence d'un modèle non mature (critères de maturité non atteints, 7 itérations). Un score ordonne; il n'affirme jamais une catégorie.
score_only:v0-immature-baseline · tel quel depuis la passe de notation : score_only signifie que le nombre peut ordonner les travaux, et qu'aucune étiquette de catégorie n'en découleClassification
machine, non validéePrédiction automatique; un appel candidat d’une seule source (Gemma direct ou Codex distillé), pas un consensus.
Le détail, modèle par modèle et score par score, se trouve en fin de page sous « Comment cette classification a été obtenue ».