Abstract Formal Specification and Verification of Computational Digital Logic Systems
Bibliographic record
Abstract
Modern computational digital logic systems, including general-purpose computer processors, make use of increasingly complex control logic and algorithms to manage the flow of data between computational elements. Formal verification methods aim to provide guarantees of correctness for this logic, but their use in practice comes with both combinatorial issues and conceptual challenges in capturing the desired behaviour in the specification language. This problem is exacerbated by the tendency to require behaviour to be specified in terms of the system state trajectory, which is often not a natural setting in which to describe the computational requirements, leading to unnecessary and problematic conceptual distance between the formal specification and the informally understood requirements. To address these issues, a novel, value-oriented approach to formal verification of these systems is proposed, which permits desired computational behaviour to be specified directly, with a conceptually simple interpretation. This approach is substantiated through an abstract modelling formalism in which computational systems can be formally described and composed from smaller components by compatibly connecting inputs and outputs; the interface of a component is described by an adapted version of polynomial functors, which captures a limited form of dependent typing that is common in real-world digital systems design. A sound but incomplete verification procedure is provided, by translating the description of each system into a novel extension of regular tree grammars which incorporates a limited form of symbolic logic and structured equality constraints, such that language inclusion implies that the system meets the specification. An inductive proof system for such language inclusion between the grammars, again sound but incomplete, is provided to enable algorithmic implementation of verification by proof search. Finally, the system descriptions are assigned category-theoretic semantics, which are used to prove the soundness of the translation to grammars and provide a formal notion of abstracting and concretizing a system between different layers of abstraction. The result of the thesis is a thorough mathematical foundation for a practical formal verification tool for computational digital logic systems. Remaining work necessary to use such a tool and address the limitations of the underlying theory in its present state is discussed.
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.009 |
| Meta-epidemiology (narrow) | 0.000 | 0.000 |
| Meta-epidemiology (broad) | 0.000 | 0.001 |
| Bibliometrics | 0.001 | 0.001 |
| Science and technology studies | 0.001 | 0.004 |
| Scholarly communication | 0.003 | 0.003 |
| Open science | 0.002 | 0.002 |
| Research integrity | 0.001 | 0.002 |
| Insufficient payload (model declined to judge) | 0.003 | 0.001 |
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".