The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4

DOI10.1007/S10817-010-9169-YzbMATH Open1216.68233OpenAlexW2003674078MaRDI QIDQ540690FDOQ540690

Authors Michael J. C. Gordon, Matt Kaufmann, Sandip Ray

Publication date 3 June 2011

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

Full work available at URL https://doi.org/10.1007/s10817-010-9169-y

zbMATH Keywords

model checkingtheorem provinglinear temporal logicautomated reasoninghigher-order logiccombining theorem provers

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Formal proofs about rewriting using ACL2
• Automatically Translating Type and Function Definitions from HOL to ACL2
• A Brief Overview of HOL4
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• scientific article; zbMATH DE number 2079835

Cites work

• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• scientific article; zbMATH DE number 2090293 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A Brief Overview of HOL4
• An ACL2 Tutorial
• Executable JVM model for analytical reasoning: A study
• Logic in Computer Science
• Structured theory development for a mechanized logic

Cited in

(1)

• Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’

Describes a project that uses

Uses Software

• ACL2
• ML
• SPIN
• HOL

This page was built for publication: The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4

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