Timeline



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 …

Mar 28, 2012:

11:44 AM Changeset [1869] by mulligan
a load of axioms closed in ASMCosts file
Note: See TracTimeline for information about the timeline view.