Timeline



Apr 27, 2012:

6:45 PM Changeset [1911] by mulligan
Changed statement of block_cost' to start on new termination argument
5:48 PM Changeset [1910] by mulligan
Finished proof modulo termination argument
10:59 AM Changeset [1909] by mulligan
Ported new statements to remainder of Interpret.ma file.

Apr 26, 2012:

5:38 PM Changeset [1908] by fguidi
notation fixup following last commit of matita we shifted the levels …
5:37 PM Changeset [1907] by mulligan
Fixes to get file to compile
5:20 PM Changeset [1906] by mulligan
Statements simplified in block_cost and dependencies
5:15 PM Changeset [1905] by boender
- plugging gap in assembly proof
5:03 PM Changeset [1904] by mulligan
Problem with proof fixed by noting that problem is actually irrelevant
4:49 PM Changeset [1903] by mulligan
Small changes prior to experiment
4:20 PM Changeset [1902] by mulligan
Reverted needless changes to StructuredTraces?
3:35 PM Changeset [1901] by mulligan
Slight changes to StructuredTraces?: should not change too much

Apr 23, 2012:

6:22 PM Changeset [1900] by mulligan
CostProof? complete, modulo some daemons and axioms in earlier files
6:10 PM Changeset [1899] by mulligan
Changes to statements of theorems
4:36 PM Changeset [1898] by mulligan
Ported changes from ASMCosts.ma into CostsProof?.ma and got everything …
3:46 PM Changeset [1897] by mulligan
Changes to proof, and pushed through those changes to rest of the file.
3:05 PM Changeset [1896] by mulligan
Finished horror proof

Apr 20, 2012:

6:40 PM Changeset [1895] by mulligan
Split the ASMCosts files while working on traverse_code_internal. A …
12:52 PM Changeset [1894] by mulligan
Closed a hole in the proof by deriving a contradiction using even_p …
11:52 AM Changeset [1893] by campbell
Show stronger result about labelling of expressions.

Apr 19, 2012:

6:09 PM Changeset [1892] by mulligan
Lots of work from today

Apr 18, 2012:

2:52 PM Changeset [1891] by mulligan
Nightmarish proofs on bitvectors. Trying to find some way of making …
2:01 PM Changeset [1890] by boender
- added comment about bitvector translation

Apr 17, 2012:

6:05 PM Changeset [1889] by boender
- some pages of article

Apr 13, 2012:

6:36 PM Changeset [1888] by campbell
Show that labelling of expressions works ... after fixing it to match …

Apr 12, 2012:

1:53 PM Changeset [1887] by boender
- added SEFM2012 directory - some progress in assembly

Apr 11, 2012:

2:36 PM Changeset [1886] by boender
- improvements for disambiguation and quick(er) typing
10:06 AM Changeset [1885] by boender
- updated assembler with new definition of occurs_exactly_once

Apr 9, 2012:

3:07 PM Changeset [1884] by campbell
Syntax changes to fit Paolo's commit.
11:53 AM Changeset [1883] by campbell
Ilias' switch removal code, plus a test.

Apr 6, 2012:

8:02 PM Changeset [1882] by tranquil
big update, alas incomplete: joint changed a bit, and all BE languages …
6:39 PM Changeset [1881] by campbell
Resurrect version of exec_up_to which shows the final state.
4:57 PM Changeset [1880] by campbell
Show that RTLabs flat traces are determined by their starting state, …

Apr 5, 2012:

6:13 PM Changeset [1879] by boender
- Policy compiles until the end, still some (fairly trivial) cases …

Apr 4, 2012:

6:48 PM Changeset [1878] by campbell
Enforce typing of constants in front-end, plus binops for RTLabs.
6:48 PM Changeset [1877] by campbell
Update RTLabs structured traces for typed binops and new memory model.
6:48 PM Changeset [1876] by campbell
Update Cexec soundness proof. Change finishes_with predicate to …
6:48 PM Changeset [1875] by campbell
Update brief memory model test.
6:48 PM Changeset [1874] by campbell
First cut at using back-end memory model throughout. Note the …
6:48 PM Changeset [1873] by campbell
Fix up earlier front-end value conversion work.
6:48 PM Changeset [1872] by campbell
Make binary operations in Cminor/RTLabs properly typed. A few extra …
1:40 PM Changeset [1871] by campbell
Change Clight to Cminor compilation to use gotos rather than loops, …

Apr 3, 2012:

2:52 PM Changeset [1870] by boender
- changed sigma00 in Assembly to use foldl_strong + proved invariants …
Note: See TracTimeline for information about the timeline view.