Timeline



Sep 20, 2012:

6:57 PM Changeset [2335] by campbell
Deal with goto labels in RTLabs to Cminor by fixing up goto statements …

Sep 16, 2012:

5:40 PM Changeset [2334] by sacerdot
Only relevant pieces of reviews left in place.
5:30 PM Changeset [2333] by sacerdot
Reviews committed.

Sep 13, 2012:

6:35 PM P1010316.JPG attached to StructuredTracesWIP by campbell
State of the whiteboard
6:32 PM StructuredTracesWIP created by campbell

Sep 12, 2012:

12:36 PM Changeset [2332] by garnier
Some progress on switch removal. Small fix in the definition of free, …

Sep 11, 2012:

5:40 PM Changeset [2331] by mulligan
Added some structure to the paper
5:11 PM Changeset [2330] by mulligan
Added directory for new structured traces paper.
5:10 PM Changeset [2329] by mulligan
Added new directory for papers so as to stop them from being spread …

Sep 10, 2012:

6:18 PM Changeset [2328] by campbell
Cut down the notion of a Clight labelled state to those where we pick …
4:45 PM Changeset [2327] by mulligan
Fixed typos in paper highlighted by referees. More substantial …

Sep 7, 2012:

12:15 PM Changeset [2326] by campbell
More accurate notion of labelled states in Clight.
11:26 AM Changeset [2325] by campbell
Fill out some Clight bits and pieces in correctness.ma.

Sep 5, 2012:

5:17 PM Changeset [2324] by tranquil
semantics of blocks: function to produce trace from execution of …
1:36 PM Changeset [2323] by campbell
Some correctness proof comments.
1:34 PM EdinburghSep2012 edited by campbell
(diff)
1:34 PM P1010314.JPG attached to EdinburghSep2012 by campbell
10:50 AM P1010310.JPG attached to EdinburghSep2012 by campbell
10:50 AM 2012-09-04 16.26.05.jpg attached to EdinburghSep2012 by campbell
10:49 AM EdinburghSep2012 created by campbell

Sep 4, 2012:

7:37 PM Changeset [2322] by campbell
Today's correctness groupthink.

Sep 3, 2012:

4:44 PM Changeset [2321] by campbell
Add toolstick branch of the prototype.
4:33 PM Changeset [2320] by campbell
Update compiler and correctness with labelling changes.
1:16 PM Changeset [2319] by campbell
Generate per-program cost labels rather than per-function ones, and …
12:42 PM Changeset [2318] by boender
- now it compiles
11:36 AM Changeset [2317] by boender
- small changes to make things compile
9:03 AM Changeset [2316] by boender
- committed temporary version: true version has to wait until I …

Aug 31, 2012:

4:52 PM Changeset [2315] by campbell
Add some more commentary.
4:12 PM Changeset [2314] by campbell
Move generic definitions from recent commit to appropriate places.
2:39 PM Changeset [2313] by campbell
RTLabs cost checker correct.
2:14 PM Changeset [2312] by garnier
Memory injections, to be revised
2:12 PM Changeset [2311] by garnier
Some more cleaning of switchRemoval …
12:50 PM Changeset [2310] by garnier
Moved a lemma from switchRemoval to positive.
11:35 AM Changeset [2309] by garnier
Removed the superfluous xorb definition and move some basic properties …

Aug 30, 2012:

7:20 PM Changeset [2308] by campbell
More proof (and corrections) on cost checking.
4:47 PM Changeset [2307] by campbell
Half the proofs for sound cost labelling check.
4:47 PM Changeset [2306] by campbell
An insertion sort for testing purposes.
4:47 PM Changeset [2305] by campbell
RTLabs cost spec checking function implemented (lacks proof, or much …

Aug 29, 2012:

11:21 PM Changeset [2304] by garnier
Strengthened proof of associativity of bitvector addition. Some more …

Aug 24, 2012:

5:41 PM Changeset [2303] by campbell
Some preliminary checking of cost labelling properties in RTLabs.
1:11 PM Changeset [2302] by garnier
Finally proved associativity of addition on bitvectors. Rejoice.

Aug 22, 2012:

5:30 PM Changeset [2301] by mulligan
Trying to get the big proof working again

Aug 21, 2012:

7:00 PM Changeset [2300] by campbell
Cut out some dead ends and add some comments to the last commit.
7:00 PM Changeset [2299] by campbell
Soundly labelled RTLabs structured traces are "unrepeating".
Note: See TracTimeline for information about the timeline view.