This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Avra Cohn
A grouping.
Avra Cohn, Cambridge HOL group: the machine-checked VIPER proofs (1987-88 reports, held in full) and their critique. Read for the caveats: a proof relates models, not the device or the intention.
7 references
The notion of proof in hardware verification
Avra Cohn (1989) · Journal of Automated Reasoning · Springer Science and Business Media LLC
Correctness properties of the Viper block model: the second level
Avra Cohn (1988) · University of Cambridge Computer Laboratory
A Proof of Correctness of the Viper Microprocessor: The First Level
Avra Cohn (1988) · VLSI Specification, Verification and Synthesis · Springer Nature
A proof of correctness of the Viper microprocessor: the first level
Avra Cohn (1987) · University of Cambridge Computer Laboratory
A mechanised proof of correctness of a simple counter
Avra Cohn and others (1986) · Technical Report 94
A Mechanized Proof of Correctness of a Simple Counter
Avra Cohn and others (1986) · University of Cambridge Computer Laboratory
High level proof in LCF
Avra Cohn (1978) · Internal Report CSR-35-78