Computer assisted reasoning. A Festschrift for Michael J. C. Gordon

DOI10.1007/s10817-009-9144-7zbMath1179.01037OpenAlexW1571821405WikidataQ125765287 ScholiaQ125765287MaRDI QIDQ2655321

Konrad Slind, Joe Hurd, Richard J. Boulton

Publication date: 25 January 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9144-7

Mathematics Subject Classification ID

Biographies, obituaries, personalia, bibliographies (01A70) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Uses Software

• ACL2
• ML
• Prosper
• Metis_
• HOL
• ProofPower
• HOL Light
• PROSPER
• Cambridge LCF

Cites Work

• Validating the PSL/Sugar semantics using automated reasoning
• The notion of proof in hardware verification
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• Proof producing synthesis of arithmetic and cryptographic hardware
• A Brief Overview of HOL4
• Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover
• Logic and Computation
• Hoare Logic for Realistically Modelled Machine Code
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Computer assisted reasoning. A Festschrift for Michael J. C. Gordon