Name | Date | Size | ||
---|---|---|---|---|
.. | 25-Jul-2019 | 13 | ||
acl2_packageScript.sml | H A D | 25-Jul-2019 | 141 KiB | |
apply-total-order.ml | H A D | 25-Jul-2019 | 15.3 KiB | |
circuit-bisim.ml | H A D | 25-Jul-2019 | 81.1 KiB | |
circuits.ml | H A D | 25-Jul-2019 | 33.8 KiB | |
complex_rationalScript.sml | H A D | 25-Jul-2019 | 12 KiB | |
cone-of-influence.ml | H A D | 25-Jul-2019 | 18.4 KiB | |
encap1.ml | H A D | 25-Jul-2019 | 5.8 KiB | |
hol_defaxiomsScript.sml | H A D | 25-Jul-2019 | 154.6 KiB | |
Holmakefile | H A D | 25-Jul-2019 | 296 | |
imported_acl2_books.ml | H A D | 25-Jul-2019 | 53 | |
load_book.sig | H A D | 25-Jul-2019 | 201 | |
load_book.sml | H A D | 25-Jul-2019 | 2.1 KiB | |
ltl-project.ml | H A D | 25-Jul-2019 | 9.4 KiB | |
ltl.ml | H A D | 25-Jul-2019 | 19.6 KiB | |
LTLScript.sml | H A D | 25-Jul-2019 | 18.9 KiB | |
mainScript.sml.save | H A D | 25-Jul-2019 | 7.3 KiB | |
make_hol_acl2_defaxioms.ml | H A D | 25-Jul-2019 | 1.3 KiB | |
make_imported_acl2_theory.ml | H A D | 25-Jul-2019 | 816 | |
make_main_theory.ml | H A D | 25-Jul-2019 | 7 KiB | |
README | H A D | 25-Jul-2019 | 2.6 KiB | |
records.ml | H A D | 25-Jul-2019 | 21.7 KiB | |
sets.ml | H A D | 25-Jul-2019 | 14.3 KiB | |
sexp.sml | H A D | 25-Jul-2019 | 112.4 KiB | |
sexpScript.sml | H A D | 25-Jul-2019 | 79.2 KiB | |
summary.ml | H A D | 25-Jul-2019 | 124.5 KiB | |
total-order.ml | H A D | 25-Jul-2019 | 3.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