The rare shared example
A subject the papers are about. The loosest grouping, and the one to reach for last.
Almost every hardware verification paper demonstrates on an example of its own choosing, which makes claims about methods very hard to weigh against each other. This set collects the exceptions: the cases where one artefact was verified more than once, so that the formalisms can be compared on something held fixed.
Membership is evidential rather than topical. The corpus must be able to see the comparison — either because it holds two or more records treating the same artefact, or because a single record sets methods against each other on one problem. Six members, in those two shapes.
**One machine, three logics, eleven years.** Gordon's computer is the best-populated shared example the corpus has. gordon1983proving verifies it in **LCF_LSM**, the hardware-specific calculus Gordon built for the purpose, as Cambridge Technical Report 42. joyce1986proving redoes the same machine in **higher order logic** and says so in its abstract — the moment the Cambridge line abandoned a special-purpose calculus for a general logic. stavridou1994gordons takes it into **OBJ3**, equational logic and algebraic specification out of the Goguen tradition, and is the only one of the three from outside that line. Rewriting against tactic-driven proof, on a machine both had already done.
**One counter, two specification styles.** cohn1986mechanized takes the counter RSRE used to illustrate its own methods and redoes it in HOL, giving both a logical specification and an **ELLA** one and verifying each. The corpus values it for that symmetry; it is also the record that made ELLA visible here long before boulton1990hol said what ELLA means.
**And two papers that are the comparison rather than a side of it.** angelo1993comparison sets HOL against **Boyer-Moore**, the two systems this corpus holds most of. tahar1998three sets HOL against **MDG** and **VIS** — deductive proof against decision diagrams against model checking — which puts the two traditions the corpus keeps in separate sets onto one artefact.
**A caution that is the point of the set, not an aside.** Four of the six can be read here and two cannot. Both of the works that are *explicitly* comparative are closed: angelo1993comparison and stavridou1994gordons are both in Formal Methods in System Design, both Springer, a year apart, and Semantic Scholar reports openAccessPdf CLOSED for each — for the Angelo paper the publisher has elided even the abstract. tahar1998three has an author copy at Queen Mary that this workstation cannot reach. So the literature's scarce comparative evidence is also its least accessible, and the corpus can say that Gordon's computer was done three ways without being able to say what the third way cost.
Overlaps what-one-proves-with, which collects works about the tools themselves; the distinction is that membership there requires the work to be about a prover, while membership here requires the *example* to be shared. A tool paper with no common artefact belongs there and not here; gordon1983proving belongs here and not there.