Timeline
Apr 30, 2013:
- 11:59 PM Changeset [3245] by
- The final pages by Michela. To be appended to the PDF generated by Ian.
- 11:50 PM Changeset [3244] by
- Final version.
- 11:34 PM Changeset [3243] by
- The report, spellchecking needed.
- 10:48 PM Changeset [3242] by
- New version with better description and copyright.
- 9:28 PM Changeset [3241] by
- Debian package for matita_0.99.2
- 7:14 PM Changeset [3240] by
- Remove Microsoft Office droppings
- 7:13 PM Changeset [3239] by
- D1.4 updates
- 7:09 PM Changeset [3238] by
- acc-trusted bumper to version 0.2.
- 7:02 PM Changeset [3237] by
- Some incomplete work on Clight -> Cminor call steps.
- 6:29 PM Changeset [3236] by
- Sneak in a single word fix.
- 6:23 PM Changeset [3235] by
- compiler tarball
- 5:39 PM Changeset [3234] by
- Debian packages committed. Some are using git, so you need to clone …
- 5:00 PM Changeset [3233] by
- passed spell checker, added description of the cerco wrapper, minor …
- 4:56 PM Changeset [3232] by
- D1.4 small changes
- 4:53 PM Changeset [3231] by
- Final revisions to 3.4.
- 4:33 PM WikiStart edited by
- (diff)
- 3:36 PM Changeset [3230] by
- Financial parts removed.
- 3:34 PM Changeset [3229] by
- numbers adjusted; only mentioned in running text under "Attendance"
- 3:22 PM Changeset [3228] by
- Add a more formal note to the abstract in 3.4.
- 1:20 PM Changeset [3227] by
- Last bits about lifting proof in 3.4.
- 12:54 PM Changeset [3226] by
- More 3.4 revisions; mostly administrative.
- 12:43 PM Changeset [3225] by
- More spelling, more grammar, more phrasing
- 12:17 PM Changeset [3224] by
- revisions…
- 12:05 PM Changeset [3223] by
- More revisions to 3.4.
- 11:45 AM Changeset [3222] by
- added pages to included papers. final version.
- 1:25 AM Changeset [3221] by
- Added cerco-executable to install.
- 12:54 AM Changeset [3220] by
- …
- 12:53 AM Changeset [3219] by
- Fixed: .in should be there.
- 12:01 AM Changeset [3218] by
- Text about Cminor to RTLabs.
Apr 29, 2013:
- 11:46 PM Changeset [3217] by
- Correctness of ERTL to LTL in place
- 11:15 PM Changeset [3216] by
- Revisions throughout 3.4.
- 9:53 PM Changeset [3215] by
- - Version dumped to 0.2 - New executable cerco to be used with why3
- 7:17 PM Changeset [3214] by
- Some 3.4 revisions.
- 6:14 PM Changeset [3213] by
- summary for D4.4, and other modifications
- 5:24 PM Changeset [3212] by
- Sort out some "to do"s, minimal conclusion.
- 5:24 PM Changeset [3211] by
- Put switch removal in correct place; describe cost labelling sim.
- 4:55 PM Changeset [3210] by
- Final version.
- 4:52 PM Changeset [3209] by
- Final version up to spelling.
- 3:36 PM Changeset [3208] by
- Final version.
- 3:31 PM Changeset [3207] by
- Final version up to spellchecking.
- 2:40 PM Changeset [3206] by
- New publication.
- 1:00 PM Changeset [3205] by
- New publication.
- 12:53 PM Changeset [3204] by
- New publication and reindentation.
- 12:39 PM Changeset [3203] by
- Text on structured trace construction.
- 11:31 AM Changeset [3202] by
- …
- 9:51 AM Changeset [3201] by
- …
- 5:32 AM Changeset [3200] by
- Final report summary
- 5:31 AM Changeset [3199] by
- D6.4/D6.5 executive summary
Apr 28, 2013:
- 6:59 PM Changeset [3198] by
- Spellchecked and reindented.
- 6:42 PM Changeset [3197] by
- Spellchecked.
- 6:40 PM Changeset [3196] by
- Spellchecked.
- 4:59 PM Changeset [3195] by
- The follow-up letter.
- 4:20 PM Changeset [3194] by
- more on the role of the stack in the back end pass. moved mauro.tex as …
- 2:53 PM Changeset [3193] by
- Completed.
Apr 27, 2013:
- 5:48 PM Changeset [3192] by
- …
- 5:00 PM Changeset [3191] by
- Some more info on cast removal
- 4:15 PM Changeset [3190] by
- …
- 4:15 PM Changeset [3189] by
- …
- 3:57 PM Changeset [3188] by
- …
- 3:57 PM Changeset [3187] by
- …
- 11:42 AM Changeset [3186] by
- …
- 11:26 AM Changeset [3185] by
- …
Apr 26, 2013:
- 7:12 PM Changeset [3184] by
- …
- 4:34 PM Changeset [3183] by
- …
- 4:22 PM Changeset [3182] by
- Part 2 completed.
- 11:08 AM Changeset [3181] by
- Compiler overview section of 3.4
Apr 25, 2013:
- 8:17 PM Changeset [3180] by
- first commit: report on back-end correctness proof
- 6:13 PM Changeset [3179] by
- …
- 6:03 PM Changeset [3178] by
- Some progress on Callstate steps in Clight to Cminor. Note that some …
- 4:10 PM Changeset [3177] by
- …
- 3:15 PM Changeset [3176] by
- simplified dependencies
- 12:34 PM Changeset [3175] by
- …
- 10:25 AM Changeset [3174] by
- …
Apr 23, 2013:
- 6:30 PM Changeset [3173] by
- A little reworking of 3.4.
Apr 20, 2013:
- 7:16 PM Changeset [3172] by
- Second section in place. Re-reading it, it seems to me worse than the …
- 9:38 AM Changeset [3171] by
- removed redundant dependencies
- 9:17 AM Changeset [3170] by
- removed redundant dependencies
Apr 19, 2013:
- 7:10 PM Changeset [3169] by
- …
- 12:30 PM Changeset [3168] by
- Add some text from Ilias.
- 12:30 PM Changeset [3167] by
- A little bit about structured traces.
- 11:58 AM Changeset [3166] by
- Questionnaire about publications filled in, DOIs added to every …
- 11:46 AM Changeset [3165] by
- A little bit of progress on Callstate case.
Apr 18, 2013:
- 10:04 PM Changeset [3164] by
- Executive report in place.
- 4:46 PM Changeset [3163] by
- All tables have been filled in.
- 4:39 PM Changeset [3162] by
- More administrative data.
- 4:21 PM Changeset [3161] by
- Tables partially filled in.
Apr 17, 2013:
- 11:38 PM Changeset [3160] by
- Initial part and description of WP2, WP3 and WP4 completed. WP5, final …
- 7:17 PM Changeset [3159] by
- A bit more text in 3.4.
- 7:17 PM Changeset [3158] by
- Some text on measurable subtraces throughout the front-end.
- 6:13 PM Changeset [3157] by
- Added tables with the workshop programmes indetail
- 3:24 PM Changeset [3156] by
- Rebuild prefix traces in back-end's preferred form.
- 3:24 PM Changeset [3155] by
- Now have proof that the initial states are in simulation for clight to …
- 2:53 PM Changeset [3154] by
- 1) changed block_of_call in order to prevent pre-main calls 2) …
Apr 16, 2013:
- 5:31 PM Changeset [3153] by
- More data.
- 2:46 PM Changeset [3152] by
- r
- 11:33 AM Changeset [3151] by
- More data flowing in.
- 11:30 AM Changeset [3150] by
- Integrated all data I received so far.
- 11:09 AM Changeset [3149] by
- More data from Roberto integrated.
- 11:00 AM Changeset [3148] by
- Infos by Roberto integrated.
Apr 15, 2013:
- 6:57 PM Changeset [3147] by
- More work on Part 4.
- 6:29 PM Changeset [3146] by
- Most of the "scientific" work required for Part4. I still need to …
- 4:31 PM Changeset [3145] by
- * removed sigma types from traces of intensional events * completed …
- 3:43 PM Changeset [3144] by
- Initial work on D1.3. Part 1 and Part 2 have been fixed already.
- 2:27 PM Changeset [3143] by
- More papers pulled into the report.
- 10:51 AM Changeset [3142] by
- Sketch out a bit more of 3.4.
Apr 12, 2013:
- 7:23 PM Changeset [3141] by
- Rephrase Tullio's contribution... more work needed?
- 7:22 PM Changeset [3140] by
- Diagram illustrating nested function calls in structured traces.
- 7:11 PM Changeset [3139] by
- English tweaks
- 7:03 PM Changeset [3138] by
- Sketch up-to-labelling bit.
- 6:53 PM Changeset [3137] by
- Tweaks
- 6:47 PM Changeset [3136] by
- Updates: form and content, incorporating comments from Brian, and from …
- 6:34 PM Changeset [3135] by
- Discussion with Kevin at HiPEAC workshop.
- 6:27 PM Changeset [3134] by
- Opps uncommitted edits!
- 6:18 PM Changeset [3133] by
- Underscores!
- 6:17 PM Changeset [3132] by
- 1st version of workshop s reports. Comments/amendments welcome!
- 6:10 PM Changeset [3131] by
- Add rest of correctness.
- 6:10 PM Changeset [3130] by
- Tweak diagram spacing.
- 6:10 PM Changeset [3129] by
- Right version of the diagram.
- 5:00 PM Changeset [3128] by
- Start of D3.4. (Sorry it's taking longer than anticipated; I blame a …
- 4:03 PM Changeset [3127] by
- report on general proof
- 1:00 AM Changeset [3126] by
- Splitted into empty report + "stand alone" paper. The paper needs to …
Apr 11, 2013:
- 7:10 PM Changeset [3125] by
- …
- 6:34 PM Changeset [3124] by
- …
- 6:22 PM Changeset [3123] by
- …
- 3:55 PM Changeset [3122] by
- …
- 3:08 PM Changeset [3121] by
- …
- 2:04 PM Changeset [3120] by
- …
Apr 10, 2013:
- 7:15 PM Changeset [3119] by
- …
- 6:45 PM Changeset [3118] by
- 1) finished return case in StatusSimulationHelper? 2) started to write …
- 6:25 PM Changeset [3117] by
- …
- 5:07 PM Changeset [3116] by
- …
- 1:28 PM Changeset [3115] by
- Clean up some left-over lemmas and move comment back into place.
- 9:48 AM Changeset [3114] by
- Some progress on pipelines/caches.
Apr 9, 2013:
- 7:00 PM Changeset [3113] by
- Some work on control flow analysis.
- 6:05 PM Changeset [3112] by
- added invariant that costlabels are only assigned to NOPs (not proved …
- 6:05 PM Changeset [3111] by
- Skeleton
- 6:02 PM Changeset [3110] by
- …
- 5:28 PM Changeset [3109] by
- New version.
Apr 8, 2013:
- 11:50 PM Changeset [3108] by
- Towards D5.2.
- 1:17 PM Changeset [3107] by
- * External tools to compile the plugin.
Apr 6, 2013:
- 7:35 PM Changeset [3106] by
- New extraction.
- 6:38 PM Changeset [3105] by
- Pretty printing changed. There is still an inefficiency left: activate …
- 6:37 PM Changeset [3104] by
- Performance improvement.
- 4:19 PM Changeset [3103] by
- Simplified "include" dependencies
- 4:11 PM Changeset [3102] by
- Removed redundant refs to current_instruction0, which itself has been …
- 4:08 PM Changeset [3101] by
- Removed redundant lemma execute_1_technical, which is covered by …
- 4:05 PM Changeset [3100] by
- Removed redundant defn of current_instruction0, which only appears in …
- 4:02 PM Changeset [3099] by
- Simplified preliminaries: inefficient_address_of_word_labels, and …
- 11:44 AM Changeset [3098] by
- Performance improvement.
Apr 5, 2013:
- 9:53 PM Changeset [3097] by
- Performance improvement in policy computation.
- 6:04 PM Changeset [3096] by
- preliminary work on closing correctness.ma
Apr 4, 2013:
- 9:53 PM Changeset [3095] by
- Some performance improvement: an heavy computation was done again and …
- 12:04 PM Changeset [3094] by
- Makefile with targets: byte opt clean
- 11:52 AM Changeset [3093] by
- Makefile replaces build, targets: byte, opt, clean
- 11:36 AM Changeset [3092] by
- No more references to Lustre stuff.
- 11:31 AM Changeset [3091] by
- …
- 11:26 AM Changeset [3090] by
- dist: take into account symlink
- 11:18 AM Changeset [3089] by
- Symbolic link to the cparser
- 11:16 AM Changeset [3088] by
- We now also generate the package for native code.
- 11:06 AM Changeset [3087] by
- script to build tarpall
- 10:53 AM Changeset [3086] by
- extracted is now in driver
- 10:46 AM Changeset [3085] by
- extracted directory moved into driver to make debian packages more …
- 10:19 AM Changeset [3084] by
- 9:58 AM Changeset [3083] by
- The cost and stack* variables are now initialized with the cost of …
- 9:31 AM Changeset [3082] by
- Tidying up: the long comment about preamble/renamed_symbols in the …
Apr 3, 2013:
- 5:54 PM Changeset [3081] by
- Tidy up recent work a little.
- 5:27 PM Changeset [3080] by
- New extraction.
- 5:03 PM Changeset [3079] by
- added printing of ERTL, LTL and LIN's ext_seq's.
- 3:01 PM Changeset [3078] by
- fixed change of Mov
- 11:49 AM Changeset [3077] by
- New extraction.
- 10:13 AM Changeset [3076] by
- simplified include dependencies
Apr 2, 2013:
- 7:59 PM Changeset [3075] by
- Apologies for late folding in of old changes which were left over from …
- 7:25 PM Changeset [3074] by
- Put some kind of high level proof in for front-end.
- 6:44 PM Changeset [3073] by
- New extraction, all tests pass.
- 6:39 PM Changeset [3072] by
- corrected a bug (translate_store was wrong)
- 4:49 PM Changeset [3071] by
- …
- 4:49 PM Changeset [3070] by
- Ext case of RTL implemented.
- 2:09 PM Changeset [3069] by
- New extraction.
- 1:51 PM Changeset [3068] by
- Debugging code removed.
- 1:49 PM Changeset [3067] by
- New test that fails too.
- 1:48 PM Changeset [3066] by
- * implemented get_arg_16 for ACC_DPTR * LINToASM is now agnostic as to …
- 1:37 PM Changeset [3065] by
- Efficiency of semantics of assembled improved: ticks_of was …
- 1:02 PM Changeset [3064] by
- Efficiency of the semantics of assembly improved by avoiding the …
- 12:16 PM Changeset [3063] by
- Remove measure function from FEMeasurable because we're not using it …
- 11:59 AM Changeset [3062] by
- Bug fixed in the semantics of Mov: the offset was ignored. Now all …
- 11:32 AM Changeset [3061] by
- New extraction.
- 11:11 AM Changeset [3060] by
- Bug fixed in the semantics of JMP. The bug was due to a bug in the …
- 1:25 AM Changeset [3059] by
- New extraction
Apr 1, 2013:
- 9:14 PM Changeset [3058] by
- …
- 9:14 PM Changeset [3057] by
- lookup of function identifiers was not corrected with sigma
- 7:17 PM Changeset [3056] by
- fixed a merge gone wrong
- 7:04 PM Changeset [3055] by
- Start getting partial Clight to Cminor proof in shape for …
- 7:04 PM Changeset [3054] by
- Put missing typ check in; adjust proof because I did it a little …
- 7:04 PM Changeset [3053] by
- Cast simplification preserves measurable subtraces.
- 6:31 PM Changeset [3052] by
- …
- 6:28 PM Changeset [3051] by
- fixed order of global initialization in LINToASM. For the moment …
- 5:18 PM Changeset [3050] by
- 1) Added general commutation theorem for monads. 2) Added some …
- 12:06 AM Changeset [3049] by
- Globalenvs and initial states for cast simplification.
- 12:06 AM Changeset [3048] by
- Improve dependency for cast simplification.
Mar 31, 2013:
- 10:01 PM Changeset [3047] by
- Switch removal and labelling combined.
Note: See TracTimeline
for information about the timeline view.