Timeline


and

05/22/13: Yesterday

09:23 Changeset [3303] by amadio
r

05/17/13:

12:15 Changeset [3302] by mckinna
removed local verison for JHM's machine wp6.tex definitive
08:35 Changeset [3301] by mckinna
updates: wp6.tex is definitive

05/16/13:

08:06 Changeset [3300] by mckinna
updates
00:51 Changeset [3299] by sacerdot
00:51 Changeset [3298] by sacerdot

05/15/13:

22:51 Changeset [3297] by tranquil
final version
22:37 Changeset [3296] by sacerdot
22:36 Changeset [3295] by sacerdot
16:18 Changeset [3294] by mckinna
draft final version: more to say than to put on slides etc.
12:39 Changeset [3293] by mckinna
more: desitination data (partial)
11:17 cpp-2011.pdf attached to WikiStart by sacerdot
11:16 WikiStart edited by sacerdot
(diff)
10:45 Changeset [3292] by mckinna
update
09:46 Changeset [3291] by mckinna
template beamer file, and notes for the talk more later today!
02:24 Changeset [3290] by stark
Minor edits to slides

05/14/13:

18:47 WikiStart edited by sacerdot
(diff)
18:43 Changeset [3289] by sacerdot
18:33 WikiStart edited by sacerdot
(diff)
17:43 D2-1-addendum.pdf attached to WikiStart by sacerdot
17:43 D4-2.pdf attached to WikiStart by sacerdot
Deliverable for D4.2
17:42 D4-3.pdf attached to WikiStart by sacerdot
Deliverable for D4.3
17:42 D5-1.pdf attached to WikiStart by sacerdot
17:42 D5-1-cost_plug_in.tgz attached to WikiStart by sacerdot
17:42 D5-1-software.tgz attached to WikiStart by sacerdot
17:41 D6.2-supplement.pdf attached to WikiStart by sacerdot
17:41 Changeset [3288] by sacerdot
The deliverables resubmitted during the third period.
17:38 D6_6.pdf attached to WikiStart by sacerdot
17:38 D6_4_D6_5.pdf attached to WikiStart by sacerdot
17:38 D6_3.pdf attached to WikiStart by sacerdot
17:38 D5_3.pdf attached to WikiStart by sacerdot
17:37 D5_2.pdf attached to WikiStart by sacerdot
17:37 D4_4.pdf attached to WikiStart by sacerdot
17:37 D3_4.pdf attached to WikiStart by sacerdot
17:36 acc_0.2.orig.tar.gz attached to WikiStart by sacerdot
17:36 acc-trusted_0.2.orig.tar.gz attached to WikiStart by sacerdot
17:36 certification_20130430.tgz attached to WikiStart by sacerdot
17:36 cost-plug-in_0.2.orig.tar.gz attached to WikiStart by sacerdot
15:58 Changeset [3287] by tranquil
back-end slides
14:39 Changeset [3286] by stark
Renaming and moving
14:38 Changeset [3285] by stark
Renaming and moving
14:33 Changeset [3284] by stark
Moving and renaming
13:05 Changeset [3283] by regisgia
* Compiled version.
13:05 Changeset [3282] by regisgia
* WP5 slides for the final review.
12:41 Changeset [3281] by tranquil
back end correctness slides, alas still incomplete
12:11 Changeset [3280] by stark
Front end final review talk?
10:47 Changeset [3279] by stark
Renaming and moving
10:46 Changeset [3278] by stark
Renaming and moving
10:45 Changeset [3277] by stark
Renaming and moving
10:45 Changeset [3276] by stark
Renaming and moving
10:44 Changeset [3275] by stark
Renaming and moving
10:38 Changeset [3274] by stark
Rnaming and moving
10:38 Changeset [3273] by stark
Rnaming and moving
10:37 Changeset [3272] by stark
Rnaming and moving
10:37 Changeset [3271] by stark
Rnaming and moving
10:37 Changeset [3270] by stark
Rnaming and moving
05:47 Changeset [3269] by stark
Some revised slides in front end, not complete

05/13/13:

19:05 Changeset [3268] by sacerdot
Presentation for WP4 by Claudio. Maybe to be moved into dissemination, but …
11:26 Changeset [3267] by campbell
Improve a few awkward parts of front-end slides.

05/10/13:

18:59 Changeset [3266] by campbell
Some f.e. revisions.
18:21 Changeset [3265] by tranquil
added validate_pointer filter in Interference added that intereference …
14:50 Changeset [3264] by campbell
Draft a bit of missing content for front-end slides.
13:40 Changeset [3263] by tranquil
moved callee saved saving and restoring to ERTL -> LTL pass (untrusted …

05/09/13:

11:31 Changeset [3262] by piccolo
reverted status_simulation_utils
11:12 Changeset [3261] by piccolo
reverted joint_semantics rtl_semantics and ltl_semantics
11:04 Changeset [3260] by campbell
Start adapting previous talk to front-end review.
00:49 Changeset [3259] by piccolo
changed ERTL semantics: 1) added manipulation of stack pointer directly in …

05/08/13:

18:38 Changeset [3258] by sacerdot
17:48 Changeset [3257] by tranquil
fixed uses in ERTL
17:41 Changeset [3256] by tranquil
fixed compilation
16:53 Changeset [3255] by tranquil
* dropped newframe and delframe (to be integrated in calls and returns in …
15:58 Changeset [3254] by sacerdot
Code I always forgot to commit. To be ported to ERTLtoLTLProof.ma.

05/06/13:

16:08 Changeset [3253] by piccolo
some proof obbligation closed of ERTL to LTL proof

05/03/13:

17:29 Changeset [3252] by piccolo
proof obbligation added on ERTL to LTL proof

05/01/13:

02:47 Changeset [3251] by sacerdot
The files submitted and the mail sent to the officer/reviewers.
02:13 Changeset [3250] by sacerdot
02:00 WikiStart edited by stark
Typofix (diff)
01:54 Changeset [3249] by stark
UEDIN D3.4, D6.4-6.5
01:40 Changeset [3248] by sacerdot
Typos fixed.
01:28 Changeset [3247] by stark
UEDIN changes to D1.3 and D1.4
01:25 WikiStart edited by sacerdot
(diff)
01:11 Changeset [3246] by sacerdot
Instructions on how to make the LiveCD.
00:28 WikiStart edited by sacerdot
(diff)
00:28 WikiStart edited by sacerdot
(diff)
00:27 cvc3_2.4.1-1_amd64.deb attached to WikiStart by sacerdot
The CVC3 theorem prover, Debian package
00:27 WikiStart edited by sacerdot
(diff)
00:14 matita_0.99.2-1_amd64.deb attached to WikiStart by sacerdot
Matita 0.99.2, compatible with the CerCo? sources. Debian package.
00:12 why3_0.73+cerco-1_amd64.deb attached to WikiStart by sacerdot
Why3 suite, Debian package.
00:11 why-examples_2.31+cerco-1_all.deb attached to WikiStart by sacerdot
Part of the why suite, modified for CerCo?. Debian package
00:11 why_2.31+cerco-1_amd64.deb attached to WikiStart by sacerdot
Part of the why suite, modified for CerCo?. Debian package
00:11 libwhy-coq_2.31+cerco-1_all.deb attached to WikiStart by sacerdot
Part of the why suite, modified for CerCo?. Debian package
00:10 frama-c-cost-plugin_0.2-1_amd64.deb attached to WikiStart by sacerdot
CerCo?'s Frama-C Cost Plugin, Debian package
00:09 acc-trusted_0.2-1_amd64.deb attached to WikiStart by sacerdot
Trusted CerCo? Compiler, Debian package
00:09 acc_0.2-1_amd64.deb attached to WikiStart by sacerdot
Untrusted CerCo? Compiler, Debian package

04/30/13:

23:59 Changeset [3245] by sacerdot
The final pages by Michela. To be appended to the PDF generated by Ian.
23:50 Changeset [3244] by sacerdot
Final version.
23:34 Changeset [3243] by sacerdot
The report, spellchecking needed.
22:48 Changeset [3242] by sacerdot
New version with better description and copyright.
21:28 Changeset [3241] by sacerdot
Debian package for matita_0.99.2
19:14 Changeset [3240] by stark
Remove Microsoft Office droppings
19:13 Changeset [3239] by stark
D1.4 updates
19:09 Changeset [3238] by sacerdot
acc-trusted bumper to version 0.2.
19:02 Changeset [3237] by campbell
Some incomplete work on Clight -> Cminor call steps.
18:29 Changeset [3236] by campbell
Sneak in a single word fix.
18:23 Changeset [3235] by tranquil
compiler tarball
17:39 Changeset [3234] by sacerdot
Debian packages committed. Some are using git, so you need to clone them …
17:00 Changeset [3233] by tranquil
passed spell checker, added description of the cerco wrapper, minor …
16:56 Changeset [3232] by stark
D1.4 small changes
16:53 Changeset [3231] by campbell
Final revisions to 3.4.
16:33 WikiStart edited by campbell
(diff)
15:36 Changeset [3230] by sacerdot
Financial parts removed.
15:34 Changeset [3229] by mckinna
numbers adjusted; only mentioned in running text under "Attendance"
15:22 Changeset [3228] by campbell
Add a more formal note to the abstract in 3.4.
13:20 Changeset [3227] by campbell
Last bits about lifting proof in 3.4.
12:54 Changeset [3226] by campbell
More 3.4 revisions; mostly administrative.
12:43 Changeset [3225] by mckinna
More spelling, more grammar, more phrasing
12:17 Changeset [3224] by mckinna
revisions…
12:05 Changeset [3223] by campbell
More revisions to 3.4.
11:45 Changeset [3222] by tranquil
added pages to included papers. final version.
01:25 Changeset [3221] by sacerdot
Added cerco-executable to install.
00:54 Changeset [3220] by sacerdot
00:53 Changeset [3219] by sacerdot
Fixed: .in should be there.
00:01 Changeset [3218] by campbell
Text about Cminor to RTLabs.

04/29/13:

23:46 Changeset [3217] by piccolo
Correctness of ERTL to LTL in place
23:15 Changeset [3216] by campbell
Revisions throughout 3.4.
21:53 Changeset [3215] by sacerdot
- Version dumped to 0.2 - New executable cerco to be used with why3
19:17 Changeset [3214] by campbell
Some 3.4 revisions.
18:14 Changeset [3213] by tranquil
summary for D4.4, and other modifications
17:24 Changeset [3212] by campbell
Sort out some "to do"s, minimal conclusion.
17:24 Changeset [3211] by campbell
Put switch removal in correct place; describe cost labelling sim.
16:55 Changeset [3210] by sacerdot
Final version.
16:52 Changeset [3209] by sacerdot
Final version up to spelling.
15:36 Changeset [3208] by sacerdot
Final version.
15:31 Changeset [3207] by sacerdot
Final version up to spellchecking.
14:40 Changeset [3206] by sacerdot
New publication.
13:00 Changeset [3205] by sacerdot
New publication.
12:53 Changeset [3204] by sacerdot
New publication and reindentation.
12:39 Changeset [3203] by campbell
Text on structured trace construction.
11:31 Changeset [3202] by sacerdot
09:51 Changeset [3201] by sacerdot
05:32 Changeset [3200] by stark
Final report summary
05:31 Changeset [3199] by stark
D6.4/D6.5 executive summary

04/28/13:

18:59 Changeset [3198] by sacerdot
Spellchecked and reindented.
18:42 Changeset [3197] by sacerdot
Spellchecked.
18:40 Changeset [3196] by sacerdot
Spellchecked.
16:59 Changeset [3195] by sacerdot
The follow-up letter.
16:20 Changeset [3194] by tranquil
more on the role of the stack in the back end pass. moved mauro.tex as an …
14:53 Changeset [3193] by sacerdot
Completed.

04/27/13:

17:48 Changeset [3192] by sacerdot
17:00 Changeset [3191] by garnier
Some more info on cast removal
16:15 Changeset [3190] by sacerdot
16:15 Changeset [3189] by sacerdot
15:57 Changeset [3188] by sacerdot
15:57 Changeset [3187] by sacerdot
11:42 Changeset [3186] by sacerdot
11:26 Changeset [3185] by sacerdot

04/26/13:

19:12 Changeset [3184] by sacerdot
16:34 Changeset [3183] by sacerdot
16:22 Changeset [3182] by sacerdot
Part 2 completed.
11:08 Changeset [3181] by campbell
Compiler overview section of 3.4

04/25/13:

20:17 Changeset [3180] by tranquil
first commit: report on back-end correctness proof
18:13 Changeset [3179] by sacerdot
18:03 Changeset [3178] by campbell
Some progress on Callstate steps in Clight to Cminor. Note that some bogus …
16:10 Changeset [3177] by sacerdot
15:15 Changeset [3176] by mckinna
simplified dependencies
12:34 Changeset [3175] by sacerdot
10:25 Changeset [3174] by sacerdot

04/23/13:

18:30 Changeset [3173] by campbell
A little reworking of 3.4.
Note: See TracTimeline for information about the timeline view.