source: src/ASM

Name Size Rev Age Author Last Change
../
CPP2011 1033   10 years sacerdot ispelled & submitted
CPP2012-asm 2327   8 years mulligan Fixed typos in paper highlighted by referees. More substantial …
TACAS2013-policy 3415   7 years boender - changes for proceedings of TACAS 2014
I8051bis.ma 125 bytes ​ 1415   9 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
README 641 bytes ​ 431   10 years mulligan - README updated - Test and DoTest? fixed to work on assembly_program - …
AssemblyAxiom.ma 1.5 KB ​ 3096   8 years tranquil preliminary work on closing correctness.ma
FoldStuff.ma 1.7 KB ​ 1600   9 years sacerdot utilities and ASM ported to the new standard library
AbstractStatus.ma 2.1 KB ​ 3100   8 years mckinna Removed redundant defn of current_instruction0, which only appears in …
UtilBranch.ma 2.4 KB ​ 2702   8 years sacerdot 1. proof closed in ASM/UtilBranch 2. more passes integrated in the …
I8051.ma 4.0 KB ​ 3255   8 years tranquil * dropped newframe and delframe (to be integrated in calls and returns …
BitVectorZ.ma 4.3 KB ​ 2200   9 years tranquil * updated joint semantics: generation of linear and graph semantics * …
OC_traces_to_exec.ma 5.3 KB ​ 3145   8 years tranquil * removed sigma types from traces of intensional events * completed …
Interpret2.ma 6.2 KB ​ 3096   8 years tranquil preliminary work on closing correctness.ma
WellLabeled.ma 6.8 KB ​ 2710   8 years sacerdot ASMCosts.ma repaired
BitVector.ma 7.1 KB ​ 2782   8 years sacerdot 1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the …
CodeMemory.ma 8.5 KB ​ 2767   8 years mckinna WARNING: BIG commit, which pushes code_size_opt check into …
ASMCostsSplit.ma 11.1 KB ​ 3145   8 years tranquil * removed sigma types from traces of intensional events * completed …
StatusProofs.ma 13.5 KB ​ 2285   8 years sacerdot 1. duplicated code erased 2. POP case finished up to lemmas on …
AssemblyProofSplitSplit.ma 15.4 KB ​ 2899   8 years sacerdot 1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …
StatusProofsSplit.ma 20.3 KB ​ 2285   8 years sacerdot 1. duplicated code erased 2. POP case finished up to lemmas on …
BitVectorTrie.ma 26.6 KB ​ 2767   8 years mckinna WARNING: BIG commit, which pushes code_size_opt check into …
CostsProof.ma 26.6 KB ​ 3145   8 years tranquil * removed sigma types from traces of intensional events * completed …
Fetch.ma 29.9 KB ​ 3099   8 years mckinna Simplified preliminaries: inefficient_address_of_word_labels, and …
PolicyFront.ma 34.2 KB ​ 3103   8 years mckinna Simplified "include" dependencies
Vector.ma 34.9 KB ​ 2286   8 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
Policy.ma 35.2 KB ​ 3078   8 years tranquil fixed change of Mov
ASMCosts.ma 37.1 KB ​ 3145   8 years tranquil * removed sigma types from traces of intensional events * completed …
Arithmetic.ma 38.3 KB ​ 3033   8 years sacerdot Bug fixed: sign_extension was extending according to the _second_ bit, …
ASM.ma 39.1 KB ​ 3112   8 years tranquil added invariant that costlabels are only assigned to NOPs (not proved …
Util.ma 41.4 KB ​ 3466   7 years asperti Removed function that is only in the standard library. Maaaany more to …
Status.ma 45.1 KB ​ 3075   8 years mckinna Apologies for late folding in of old changes which were left over from …
AssemblyProof.ma 54.1 KB ​ 2899   8 years sacerdot 1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …
Interpret.ma 60.1 KB ​ 3101   8 years mckinna Removed redundant lemma execute_1_technical, which is covered by …
Assembly.ma 60.3 KB ​ 3112   8 years tranquil added invariant that costlabels are only assigned to NOPs (not proved …
PolicyStep.ma 61.0 KB ​ 3097   8 years sacerdot Performance improvement in policy computation.
Test.ma 92.8 KB ​ 2284   8 years sacerdot PUSH finished
AssemblyProofSplit.ma 119.7 KB ​ 2516   8 years mckinna removed typedefs; restored older versions; moved typedefs to …
Note: See TracBrowser for help on using the repository browser.