|
|
@3273
|
8 years |
Ian Stark |
Rnaming and moving
|
|
|
@3272
|
8 years |
Ian Stark |
Rnaming and moving
|
|
|
@3271
|
8 years |
Ian Stark |
Rnaming and moving
|
|
|
@3270
|
8 years |
Ian Stark |
Rnaming and moving
|
|
|
@3269
|
8 years |
Ian Stark |
Some revised slides in front end, not complete
|
|
|
@3268
|
8 years |
sacerdot |
Presentation for WP4 by Claudio.
Maybe to be moved into dissemination, …
|
|
|
@3267
|
8 years |
campbell |
Improve a few awkward parts of front-end slides.
|
|
|
@3266
|
8 years |
campbell |
Some f.e. revisions.
|
|
|
@3265
|
8 years |
tranquil |
added validate_pointer filter
in Interference added that intereference …
|
|
|
@3264
|
8 years |
campbell |
Draft a bit of missing content for front-end slides.
|
|
|
@3263
|
8 years |
tranquil |
moved callee saved saving and restoring to ERTL -> LTL pass (untrusted …
|
|
|
@3262
|
8 years |
piccolo |
reverted status_simulation_utils
|
|
|
@3261
|
8 years |
piccolo |
reverted joint_semantics rtl_semantics and ltl_semantics
|
|
|
@3260
|
8 years |
campbell |
Start adapting previous talk to front-end review.
|
|
|
@3259
|
8 years |
piccolo |
changed ERTL semantics:
1) added manipulation of stack pointer …
|
|
|
@3258
|
8 years |
sacerdot |
…
|
|
|
@3257
|
8 years |
tranquil |
fixed uses in ERTL
|
|
|
@3256
|
8 years |
tranquil |
fixed compilation
|
|
|
@3255
|
8 years |
tranquil |
* dropped newframe and delframe (to be integrated in calls and returns …
|
|
|
@3254
|
8 years |
sacerdot |
Code I always forgot to commit.
To be ported to ERTLtoLTLProof.ma.
|
|
|
@3253
|
8 years |
piccolo |
some proof obbligation closed of ERTL to LTL proof
|
|
|
@3252
|
8 years |
piccolo |
proof obbligation added on ERTL to LTL proof
|
|
|
@3251
|
8 years |
sacerdot |
The files submitted and the mail sent to the officer/reviewers.
|
|
|
@3250
|
8 years |
sacerdot |
…
|
|
|
@3249
|
8 years |
Ian Stark |
UEDIN D3.4, D6.4-6.5
|
|
|
@3248
|
8 years |
sacerdot |
Typos fixed.
|
|
|
@3247
|
8 years |
Ian Stark |
UEDIN changes to D1.3 and D1.4
|
|
|
@3246
|
8 years |
sacerdot |
Instructions on how to make the LiveCD.
|
|
|
@3245
|
8 years |
sacerdot |
The final pages by Michela. To be appended to the PDF generated by Ian.
|
|
|
@3244
|
8 years |
sacerdot |
Final version.
|
|
|
@3243
|
8 years |
sacerdot |
The report, spellchecking needed.
|
|
|
@3242
|
8 years |
sacerdot |
New version with better description and copyright.
|
|
|
@3241
|
8 years |
sacerdot |
Debian package for matita_0.99.2
|
|
|
@3240
|
8 years |
Ian Stark |
Remove Microsoft Office droppings
|
|
|
@3239
|
8 years |
Ian Stark |
D1.4 updates
|
|
|
@3238
|
8 years |
sacerdot |
acc-trusted bumper to version 0.2.
|
|
|
@3237
|
8 years |
campbell |
Some incomplete work on Clight -> Cminor call steps.
|
|
|
@3236
|
8 years |
campbell |
Sneak in a single word fix.
|
|
|
@3235
|
8 years |
tranquil |
compiler tarball
|
|
|
@3234
|
8 years |
sacerdot |
Debian packages committed.
Some are using git, so you need to clone …
|
|
|
@3233
|
8 years |
tranquil |
passed spell checker, added description of the cerco wrapper, minor …
|
|
|
@3232
|
8 years |
Ian Stark |
D1.4 small changes
|
|
|
@3231
|
8 years |
campbell |
Final revisions to 3.4.
|
|
|
@3230
|
8 years |
sacerdot |
Financial parts removed.
|
|
|
@3229
|
8 years |
mckinna |
numbers adjusted; only mentioned in running text under "Attendance"
|
|
|
@3228
|
8 years |
campbell |
Add a more formal note to the abstract in 3.4.
|
|
|
@3227
|
8 years |
campbell |
Last bits about lifting proof in 3.4.
|
|
|
@3226
|
8 years |
campbell |
More 3.4 revisions; mostly administrative.
|
|
|
@3225
|
8 years |
mckinna |
More spelling, more grammar, more phrasing
|
|
|
@3224
|
8 years |
mckinna |
revisions…
|
|
|
@3223
|
8 years |
campbell |
More revisions to 3.4.
|
|
|
@3222
|
8 years |
tranquil |
added pages to included papers. final version.
|
|
|
@3221
|
8 years |
sacerdot |
Added cerco-executable to install.
|
|
|
@3220
|
8 years |
sacerdot |
…
|
|
|
@3219
|
8 years |
sacerdot |
Fixed: .in should be there.
|
|
|
@3218
|
8 years |
campbell |
Text about Cminor to RTLabs.
|
|
|
@3217
|
8 years |
piccolo |
Correctness of ERTL to LTL in place
|
|
|
@3216
|
8 years |
campbell |
Revisions throughout 3.4.
|
|
|
@3215
|
8 years |
sacerdot |
- Version dumped to 0.2
- New executable cerco to be used with why3
|
|
|
@3214
|
8 years |
campbell |
Some 3.4 revisions.
|
|
|
@3213
|
8 years |
tranquil |
summary for D4.4, and other modifications
|
|
|
@3212
|
8 years |
campbell |
Sort out some "to do"s, minimal conclusion.
|
|
|
@3211
|
8 years |
campbell |
Put switch removal in correct place; describe cost labelling sim.
|
|
|
@3210
|
8 years |
sacerdot |
Final version.
|
|
|
@3209
|
8 years |
sacerdot |
Final version up to spelling.
|
|
|
@3208
|
8 years |
sacerdot |
Final version.
|
|
|
@3207
|
8 years |
sacerdot |
Final version up to spellchecking.
|
|
|
@3206
|
8 years |
sacerdot |
New publication.
|
|
|
@3205
|
8 years |
sacerdot |
New publication.
|
|
|
@3204
|
8 years |
sacerdot |
New publication and reindentation.
|
|
|
@3203
|
8 years |
campbell |
Text on structured trace construction.
|
|
|
@3202
|
8 years |
sacerdot |
…
|
|
|
@3201
|
8 years |
sacerdot |
…
|
|
|
@3200
|
8 years |
Ian Stark |
Final report summary
|
|
|
@3199
|
8 years |
Ian Stark |
D6.4/D6.5 executive summary
|
|
|
@3198
|
8 years |
sacerdot |
Spellchecked and reindented.
|
|
|
@3197
|
8 years |
sacerdot |
Spellchecked.
|
|
|
@3196
|
8 years |
sacerdot |
Spellchecked.
|
|
|
@3195
|
8 years |
sacerdot |
The follow-up letter.
|
|
|
@3194
|
8 years |
tranquil |
more on the role of the stack in the back end pass.
moved mauro.tex as …
|
|
|
@3193
|
8 years |
sacerdot |
Completed.
|
|
|
@3192
|
8 years |
sacerdot |
…
|
|
|
@3191
|
8 years |
garnier |
Some more info on cast removal
|
|
|
@3190
|
8 years |
sacerdot |
…
|
|
|
@3189
|
8 years |
sacerdot |
…
|
|
|
@3188
|
8 years |
sacerdot |
…
|
|
|
@3187
|
8 years |
sacerdot |
…
|
|
|
@3186
|
8 years |
sacerdot |
…
|
|
|
@3185
|
8 years |
sacerdot |
…
|
|
|
@3184
|
8 years |
sacerdot |
…
|
|
|
@3183
|
8 years |
sacerdot |
…
|
|
|
@3182
|
8 years |
sacerdot |
Part 2 completed.
|
|
|
@3181
|
8 years |
campbell |
Compiler overview section of 3.4
|
|
|
@3180
|
8 years |
tranquil |
first commit: report on back-end correctness proof
|
|
|
@3179
|
8 years |
sacerdot |
…
|
|
|
@3178
|
8 years |
campbell |
Some progress on Callstate steps in Clight to Cminor.
Note that some …
|
|
|
@3177
|
8 years |
sacerdot |
…
|
|
|
@3176
|
8 years |
mckinna |
simplified dependencies
|
|
|
@3175
|
8 years |
sacerdot |
…
|
|
|
@3174
|
8 years |
sacerdot |
…
|
|
|