Timeline


and

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) …

Apr 16, 2013:

5:31 PM Changeset [3153] by sacerdot
More data.
2:46 PM Changeset [3152] by amadio
r
11:33 AM Changeset [3151] by sacerdot
More data flowing in.
11:30 AM Changeset [3150] by sacerdot
Integrated all data I received so far.
11:09 AM Changeset [3149] by sacerdot
More data from Roberto integrated.
11:00 AM Changeset [3148] by sacerdot
Infos by Roberto integrated.

Apr 15, 2013:

6:57 PM Changeset [3147] by sacerdot
More work on Part 4.
6:29 PM Changeset [3146] by sacerdot
Most of the "scientific" work required for Part4. I still need to …
4:31 PM Changeset [3145] by tranquil
* removed sigma types from traces of intensional events * completed …
3:43 PM Changeset [3144] by sacerdot
Initial work on D1.3. Part 1 and Part 2 have been fixed already.
2:27 PM Changeset [3143] by sacerdot
More papers pulled into the report.
10:51 AM Changeset [3142] by campbell
Sketch out a bit more of 3.4.

Apr 12, 2013:

7:23 PM Changeset [3141] by mckinna
Rephrase Tullio's contribution... more work needed?
7:22 PM Changeset [3140] by campbell
Diagram illustrating nested function calls in structured traces.
7:11 PM Changeset [3139] by mckinna
English tweaks
7:03 PM Changeset [3138] by campbell
Sketch up-to-labelling bit.
6:53 PM Changeset [3137] by mckinna
Tweaks
6:47 PM Changeset [3136] by mckinna
Updates: form and content, incorporating comments from Brian, and from …
6:34 PM Changeset [3135] by campbell
Discussion with Kevin at HiPEAC workshop.
6:27 PM Changeset [3134] by mckinna
Opps uncommitted edits!
6:18 PM Changeset [3133] by mckinna
Underscores!
6:17 PM Changeset [3132] by mckinna
1st version of workshop s reports. Comments/amendments welcome!
6:10 PM Changeset [3131] by campbell
Add rest of correctness.
6:10 PM Changeset [3130] by campbell
Tweak diagram spacing.
6:10 PM Changeset [3129] by campbell
Right version of the diagram.
5:00 PM Changeset [3128] by campbell
Start of D3.4. (Sorry it's taking longer than anticipated; I blame a …
4:03 PM Changeset [3127] by piccolo
report on general proof
1:00 AM Changeset [3126] by sacerdot
Splitted into empty report + "stand alone" paper. The paper needs to …

Apr 11, 2013:

7:10 PM Changeset [3125] by sacerdot
6:34 PM Changeset [3124] by sacerdot
6:22 PM Changeset [3123] by sacerdot
3:55 PM Changeset [3122] by sacerdot
3:08 PM Changeset [3121] by sacerdot
2:04 PM Changeset [3120] by sacerdot

Apr 10, 2013:

7:15 PM Changeset [3119] by sacerdot
6:45 PM Changeset [3118] by piccolo
1) finished return case in StatusSimulationHelper? 2) started to write …
6:25 PM Changeset [3117] by sacerdot
5:07 PM Changeset [3116] by sacerdot
1:28 PM Changeset [3115] by campbell
Clean up some left-over lemmas and move comment back into place.
9:48 AM Changeset [3114] by sacerdot
Some progress on pipelines/caches.
9:39 AM cost-plug-in-0.2.tgz attached to WikiStart by regisgia
Frama-C (Nitrogen) Cost plugin

Apr 9, 2013:

7:00 PM Changeset [3113] by sacerdot
Some work on control flow analysis.
6:05 PM Changeset [3112] by tranquil
added invariant that costlabels are only assigned to NOPs (not proved …
6:05 PM Changeset [3111] by sacerdot
Skeleton
6:02 PM Changeset [3110] by sacerdot
5:28 PM Changeset [3109] by sacerdot
New version.

Apr 8, 2013:

11:50 PM Changeset [3108] by sacerdot
Towards D5.2.
1:17 PM Changeset [3107] by regisgia
* External tools to compile the plugin.

Apr 6, 2013:

7:35 PM Changeset [3106] by sacerdot
New extraction.
6:38 PM Changeset [3105] by sacerdot
Pretty printing changed. There is still an inefficiency left: activate …
6:37 PM Changeset [3104] by sacerdot
Performance improvement.
4:19 PM Changeset [3103] by mckinna
Simplified "include" dependencies
4:11 PM Changeset [3102] by mckinna
Removed redundant refs to current_instruction0, which itself has been …
4:08 PM Changeset [3101] by mckinna
Removed redundant lemma execute_1_technical, which is covered by …
4:05 PM Changeset [3100] by mckinna
Removed redundant defn of current_instruction0, which only appears in …
4:02 PM Changeset [3099] by mckinna
Simplified preliminaries: inefficient_address_of_word_labels, and …
11:44 AM Changeset [3098] by sacerdot
Performance improvement.

Apr 5, 2013:

9:53 PM Changeset [3097] by sacerdot
Performance improvement in policy computation.
6:04 PM Changeset [3096] by tranquil
preliminary work on closing correctness.ma

Apr 4, 2013:

9:53 PM Changeset [3095] by sacerdot
Some performance improvement: an heavy computation was done again and …
12:04 PM Changeset [3094] by sacerdot
Makefile with targets: byte opt clean
11:52 AM Changeset [3093] by sacerdot
Makefile replaces build, targets: byte, opt, clean
11:36 AM Changeset [3092] by sacerdot
No more references to Lustre stuff.
11:31 AM Changeset [3091] by sacerdot
11:26 AM Changeset [3090] by tassi
dist: take into account symlink
11:18 AM Changeset [3089] by sacerdot
Symbolic link to the cparser
11:16 AM Changeset [3088] by sacerdot
We now also generate the package for native code.
11:06 AM Changeset [3087] by tassi
script to build tarpall
10:53 AM Changeset [3086] by sacerdot
extracted is now in driver
10:46 AM Changeset [3085] by sacerdot
extracted directory moved into driver to make debian packages more …
10:19 AM Changeset [3084] by amadio
9:58 AM Changeset [3083] by sacerdot
The cost and stack* variables are now initialized with the cost of …
9:31 AM Changeset [3082] by mckinna
Tidying up: the long comment about preamble/renamed_symbols in the …

Apr 3, 2013:

5:54 PM Changeset [3081] by campbell
Tidy up recent work a little.
5:27 PM Changeset [3080] by sacerdot
New extraction.
5:03 PM Changeset [3079] by tranquil
added printing of ERTL, LTL and LIN's ext_seq's.
3:01 PM Changeset [3078] by tranquil
fixed change of Mov
11:49 AM Changeset [3077] by sacerdot
New extraction.
10:13 AM Changeset [3076] by mckinna
simplified include dependencies

Apr 2, 2013:

7:59 PM Changeset [3075] by mckinna
Apologies for late folding in of old changes which were left over from …
7:25 PM Changeset [3074] by campbell
Put some kind of high level proof in for front-end.
6:44 PM Changeset [3073] by sacerdot
New extraction, all tests pass.
6:39 PM Changeset [3072] by tranquil
corrected a bug (translate_store was wrong)
4:49 PM Changeset [3071] by sacerdot
4:49 PM Changeset [3070] by sacerdot
Ext case of RTL implemented.
2:09 PM Changeset [3069] by sacerdot
New extraction.
1:51 PM Changeset [3068] by sacerdot
Debugging code removed.
1:49 PM Changeset [3067] by sacerdot
New test that fails too.
1:48 PM Changeset [3066] by tranquil
* implemented get_arg_16 for ACC_DPTR * LINToASM is now agnostic as to …
1:37 PM Changeset [3065] by sacerdot
Efficiency of semantics of assembled improved: ticks_of was …
1:02 PM Changeset [3064] by sacerdot
Efficiency of the semantics of assembly improved by avoiding the …
12:16 PM Changeset [3063] by campbell
Remove measure function from FEMeasurable because we're not using it …
11:59 AM Changeset [3062] by sacerdot
Bug fixed in the semantics of Mov: the offset was ignored. Now all …
11:32 AM Changeset [3061] by sacerdot
New extraction.
11:11 AM Changeset [3060] by sacerdot
Bug fixed in the semantics of JMP. The bug was due to a bug in the …
1:25 AM Changeset [3059] by sacerdot
New extraction

Apr 1, 2013:

9:14 PM Changeset [3058] by tranquil
9:14 PM Changeset [3057] by tranquil
lookup of function identifiers was not corrected with sigma
7:17 PM Changeset [3056] by tranquil
fixed a merge gone wrong
7:04 PM Changeset [3055] by campbell
Start getting partial Clight to Cminor proof in shape for …
7:04 PM Changeset [3054] by campbell
Put missing typ check in; adjust proof because I did it a little …
7:04 PM Changeset [3053] by campbell
Cast simplification preserves measurable subtraces.
6:31 PM Changeset [3052] by tranquil
6:28 PM Changeset [3051] by tranquil
fixed order of global initialization in LINToASM. For the moment …
5:18 PM Changeset [3050] by piccolo
1) Added general commutation theorem for monads. 2) Added some …
12:06 AM Changeset [3049] by campbell
Globalenvs and initial states for cast simplification.
12:06 AM Changeset [3048] by campbell
Improve dependency for cast simplification.
Note: See TracTimeline for information about the timeline view.