#
0a22b59a |
|
17-Aug-2009 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Self-contained example to support a paper, provisionally entitled "The Right Tools for the Job: A Case Study Using ACL2 and HOL4", being written by Mike Gordon, Matt Kaufmann and Sandip Ray. The paper describes using a Linear Temporal Logic (LTL) theory in HOL to prove a correctness property of an ACL2 cone of influence reduction tool implemented in ACL2.See: http://www.cs.utexas.edu/~sandip/publications/ltl-reductions/main.html The HOL proof (including building the HOL model of the ACL2 logic) should run to completion from an invocation of Holmake. See the READ-ME file for more details.
|