../
|
CPP2011
|
|
1033
|
10 years
|
sacerdot |
ispelled & submitted
|
CPP2012-asm
|
|
2327
|
8 years
|
mulligan |
Fixed typos in paper highlighted by referees. More substantial …
|
CPP2012-policy
|
|
2099
|
9 years
|
boender |
- added reference to Intel dev manual
|
AbstractStatus.ma
|
2.0 KB
|
2705
|
8 years
|
sacerdot |
More progress in ASM towards implementing the new pseudoinstructions.
|
Arithmetic.ma
|
37.4 KB
|
2700
|
8 years
|
sacerdot |
1. exponential function dropped in favour of standard library
2. …
|
ASM.ma
|
32.7 KB
|
2708
|
8 years
|
tranquil |
fixed linearise and LINToASM
LINToASM has now correct transformation …
|
ASMCosts.ma
|
37.0 KB
|
2710
|
8 years
|
sacerdot |
ASMCosts.ma repaired
|
ASMCostsSplit.ma
|
12.1 KB
|
2665
|
8 years
|
sacerdot |
…
|
Assembly.ma
|
49.6 KB
|
2707
|
8 years
|
sacerdot |
Assembly repaired.
|
AssemblyProof.ma
|
62.0 KB
|
2516
|
8 years
|
mckinna |
removed typedefs; restored older versions; moved typedefs to …
|
AssemblyProofSplit.ma
|
119.7 KB
|
2516
|
8 years
|
mckinna |
removed typedefs; restored older versions; moved typedefs to …
|
AssemblyProofSplitSplit.ma
|
15.5 KB
|
2278
|
8 years
|
mulligan |
Half of JC case complete
|
BitVector.ma
|
7.6 KB
|
2645
|
8 years
|
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
BitVectorTrie.ma
|
25.7 KB
|
2028
|
9 years
|
boender |
- bugfix to Assembly (forgotten sigma)
- added …
|
BitVectorZ.ma
|
4.3 KB
|
2200
|
9 years
|
tranquil |
* updated joint semantics: generation of linear and graph semantics
* …
|
CostsProof.ma
|
34.6 KB
|
2671
|
8 years
|
sacerdot |
simplification
|
Fetch.ma
|
32.4 KB
|
2516
|
8 years
|
mckinna |
removed typedefs; restored older versions; moved typedefs to …
|
FoldStuff.ma
|
1.7 KB
|
1600
|
9 years
|
sacerdot |
utilities and ASM ported to the new standard library
|
I8051.ma
|
4.6 KB
|
2645
|
8 years
|
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
I8051bis.ma
|
125 bytes
|
1415
|
9 years
|
sacerdot |
1. hwreg_store/retrieve no longer returns a res (but it is still …
|
Interpret2.ma
|
2.4 KB
|
2516
|
8 years
|
mckinna |
removed typedefs; restored older versions; moved typedefs to …
|
Interpret.ma
|
60.1 KB
|
2705
|
8 years
|
sacerdot |
More progress in ASM towards implementing the new pseudoinstructions.
|
Policy.ma
|
35.6 KB
|
2745
|
8 years
|
sacerdot |
1. Complexity of policy computation lowered from O(n2) to O(n)
2. …
|
PolicyFront.ma
|
33.4 KB
|
2713
|
8 years
|
sacerdot |
PolicyFront?.ma repaired
|
PolicyStep.ma
|
59.8 KB
|
2714
|
8 years
|
sacerdot |
PolicyStep?.ma repaired
|
README
|
641 bytes
|
431
|
10 years
|
mulligan |
- README updated
- Test and DoTest? fixed to work on assembly_program
- …
|
Status.ma
|
38.4 KB
|
2710
|
8 years
|
sacerdot |
ASMCosts.ma repaired
|
StatusProofs.ma
|
13.5 KB
|
2285
|
8 years
|
sacerdot |
1. duplicated code erased
2. POP case finished up to lemmas on …
|
StatusProofsSplit.ma
|
20.3 KB
|
2285
|
8 years
|
sacerdot |
1. duplicated code erased
2. POP case finished up to lemmas on …
|
Test.ma
|
92.8 KB
|
2284
|
8 years
|
sacerdot |
PUSH finished
|
Util.ma
|
41.5 KB
|
2700
|
8 years
|
sacerdot |
1. exponential function dropped in favour of standard library
2. …
|
UtilBranch.ma
|
2.4 KB
|
2702
|
8 years
|
sacerdot |
1. proof closed in ASM/UtilBranch
2. more passes integrated in the …
|
Vector.ma
|
34.9 KB
|
2286
|
8 years
|
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
WellLabeled.ma
|
6.8 KB
|
2710
|
8 years
|
sacerdot |
ASMCosts.ma repaired
|