Bibliographic record
Abstract
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.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.003 | 0.016 |
| Meta-epidemiology (narrow) | 0.002 | 0.001 |
| Meta-epidemiology (broad) | 0.002 | 0.001 |
| Bibliometrics | 0.002 | 0.001 |
| Science and technology studies | 0.002 | 0.001 |
| Scholarly communication | 0.006 | 0.004 |
| Open science | 0.002 | 0.001 |
| Research integrity | 0.006 | 0.009 |
| Insufficient payload (model declined to judge) | 0.046 | 0.040 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".