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

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

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)

Cites Work

• A Brief Overview of HOL4
• Title not available (Why is that?)
• Logic in Computer Science
• Structured theory development for a mechanized logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Executable JVM model for analytical reasoning: A study
• An ACL2 Tutorial

Cited In (1)

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

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)