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

DOI10.1007/S10817-009-9144-7MaRDI QIDQ2655321zbMATH OpenOpenAlexWikidataFDO

Authors Joe Hurd, Konrad Slind, Richard 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) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• A Brief Overview of HOL4
• Edinburgh LCF. A mechanized logic of computation
• Hoare Logic for Realistically Modelled Machine Code
• scientific article; zbMATH DE number 1629957 (Why is no real title available?)
• scientific article; zbMATH DE number 1670743 (Why is no real title available?)
• scientific article; zbMATH DE number 2185697 (Why is no real title available?)
• scientific article; zbMATH DE number 2127501 (Why is no real title available?)
• scientific article; zbMATH DE number 3991418 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 53982 (Why is no real title available?)
• scientific article; zbMATH DE number 3640837 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Logic and Computation
• Programming a symbolic model checker in a fully expansive theorem prover
• Proof producing synthesis of arithmetic and cryptographic hardware
• The notion of proof in hardware verification
• Validating the PSL/Sugar semantics using automated reasoning

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2655321)