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

DOI10.1007/S10817-010-9169-YzbMath1216.68233OpenAlexW2003674078MaRDI QIDQ540690

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

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

theorem provingautomated reasoninghigher-order logicmodel checkinglinear temporal logiccombining theorem provers

Mathematics Subject Classification ID

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

Related Items (1)

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

Uses Software

• Unnamed Item
• Unnamed Item
• SPIN
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Structured theory development for a mechanized logic
• Executable JVM model for analytical reasoning: A study
• An ACL2 Tutorial
• A Brief Overview of HOL4
• Logic in Computer Science

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