The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
From MaRDI portal
Publication:540690
DOI10.1007/s10817-010-9169-yzbMath1216.68233MaRDI QIDQ540690
Matt Kaufmann, Michael J. C. Gordon, 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
theorem proving; automated reasoning; higher-order logic; model checking; linear temporal logic; combining theorem provers
Uses Software