NameDateSize

..25-Jul-201913

acl2_packageScript.smlH A D25-Jul-2019141 KiB

apply-total-order.mlH A D25-Jul-201915.3 KiB

circuit-bisim.mlH A D25-Jul-201981.1 KiB

circuits.mlH A D25-Jul-201933.8 KiB

complex_rationalScript.smlH A D25-Jul-201912 KiB

cone-of-influence.mlH A D25-Jul-201918.4 KiB

encap1.mlH A D25-Jul-20195.8 KiB

hol_defaxiomsScript.smlH A D25-Jul-2019154.6 KiB

HolmakefileH A D25-Jul-2019296

imported_acl2_books.mlH A D25-Jul-201953

load_book.sigH A D25-Jul-2019201

load_book.smlH A D25-Jul-20192.1 KiB

ltl-project.mlH A D25-Jul-20199.4 KiB

ltl.mlH A D25-Jul-201919.6 KiB

LTLScript.smlH A D25-Jul-201918.9 KiB

mainScript.sml.saveH A D25-Jul-20197.3 KiB

make_hol_acl2_defaxioms.mlH A D25-Jul-20191.3 KiB

make_imported_acl2_theory.mlH A D25-Jul-2019816

make_main_theory.mlH A D25-Jul-20197 KiB

READMEH A D25-Jul-20192.6 KiB

records.mlH A D25-Jul-201921.7 KiB

sets.mlH A D25-Jul-201914.3 KiB

sexp.smlH A D25-Jul-2019112.4 KiB

sexpScript.smlH A D25-Jul-201979.2 KiB

summary.mlH A D25-Jul-2019124.5 KiB

total-order.mlH A D25-Jul-20193.6 KiB

README

1This directory contains everything for performing the HOL part of the
2HOL-ACL2 proof of the soundness with respect to HOL LTL semantics of
3the Ray et al ACL2 of a cone of influence algorithm. See:
4
5 Sandip Ray, John Matthews, Mark Tuttle, 
6 "Certifying Compositional Model Checking Algorithms in ACL2"
7
8All the general ACL2-in-HOL support files are in this directory as
9well as the particular files for the LTL.
10
11   READ-ME ............................... This file
12
13   Holmakefile ........................... Instructions interpreted by Holmake
14   Holmake.log ........................... Log of Holmake
15
16   complex_rationalScript.sml ............ Script to build theory of complex rationals
17   sexpScript.sml ........................ Script to build theory of s-expressions
18   acl2_packageScript.sml ................ Script to build and validate package specification
19   hol_defaxiomsScript.sml ............... HOL definitions of functions in defaxioms
20   sexp.sml .............................. Tool for interactively processing s-expressions
21   load_book.sml ......................... Load an ACL2-generated ML book into HOL
22   make_hol_acl2_defaxioms.ml ............ Creates and writes file hol_acl2_defaxioms.lisp
23
24   LTLScript.sml ......................... Script to build LTL semantics and bisumulation theorem
25
26   summary.ml ............................ Imported from ACL2
27   ltl-project.ml ........................ Imported from ACL2
28   encap1.ml ............................. Imported from ACL2
29   records.ml ............................ Imported from ACL2
30   circuits.ml ........................... Imported from ACL2
31   cone-of-influence.ml .................. Imported from ACL2
32   ltl.ml ................................ Imported from ACL2
33   circuit-bisim.ml ...................... Imported from ACL2
34   total-order.ml ........................ Imported from ACL2
35   sets.ml ............................... Imported from ACL2
36   apply-total-order.ml .................. Imported from ACL2
37
38   load_book.sig ......................... Signature for load_book.sml
39   imported_acl2_books.ml ................ List of top level ACL2 books to be imported
40   make_imported_acl2_theory.ml .......... Makes imported_acl2Theory from imported ACL2
41   make_main_theory.ml ................... Script to make mainTheory (to be replaced by mainScript.sml)
42
43Holmake will perform the complete proof, including rebuilding the
44HOL-ACL2 infrastructure. Current Holmakefile is a hack to get around
45mysterious failure of an attempt to write mainScript.sml (to replace
46make_main_theory.ml).
47
48MJCG
49Mon Aug 17 11:27:43 BST 2009
50