Timeline


and

May 17, 2013:

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

May 16, 2013:

8:06 AM Changeset [3300] by mckinna
updates
12:51 AM Changeset [3299] by sacerdot
12:51 AM Changeset [3298] by sacerdot

May 15, 2013:

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

May 14, 2013:

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

May 13, 2013:

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

May 10, 2013:

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

May 9, 2013:

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

May 8, 2013:

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

May 6, 2013:

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

May 3, 2013:

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

May 1, 2013:

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

Apr 30, 2013:

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

Apr 29, 2013:

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

Apr 28, 2013:

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

Apr 27, 2013:

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

Apr 26, 2013:

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

Apr 25, 2013:

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

Apr 23, 2013:

6:30 PM Changeset [3173] by campbell
A little reworking of 3.4.

Apr 20, 2013:

7:16 PM Changeset [3172] by sacerdot
Second section in place. Re-reading it, it seems to me worse than the …
9:38 AM Changeset [3171] by mckinna
removed redundant dependencies
9:17 AM Changeset [3170] by mckinna
removed redundant dependencies

Apr 19, 2013:

7:10 PM Changeset [3169] by sacerdot
12:30 PM Changeset [3168] by campbell
Add some text from Ilias.
12:30 PM Changeset [3167] by campbell
A little bit about structured traces.
11:58 AM Changeset [3166] by sacerdot
Questionnaire about publications filled in, DOIs added to every …
11:46 AM Changeset [3165] by campbell
A little bit of progress on Callstate case.

Apr 18, 2013:

10:04 PM Changeset [3164] by sacerdot
Executive report in place.
4:46 PM Changeset [3163] by sacerdot
All tables have been filled in.
4:39 PM Changeset [3162] by sacerdot
More administrative data.
4:21 PM Changeset [3161] by sacerdot
Tables partially filled in.

Apr 17, 2013:

11:38 PM Changeset [3160] by sacerdot
Initial part and description of WP2, WP3 and WP4 completed. WP5, final …
7:17 PM Changeset [3159] by campbell
A bit more text in 3.4.
7:17 PM Changeset [3158] by campbell
Some text on measurable subtraces throughout the front-end.
6:13 PM Changeset [3157] by mckinna
Added tables with the workshop programmes indetail
3:24 PM Changeset [3156] by campbell
Rebuild prefix traces in back-end's preferred form.
3:24 PM Changeset [3155] by campbell
Now have proof that the initial states are in simulation for clight to …
2:53 PM Changeset [3154] by piccolo
1) changed block_of_call in order to prevent pre-main calls 2) …
Note: See TracTimeline for information about the timeline view.