Timeline



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.