

@3315

8 years 
sacerdot 
…



@3314

8 years 
sacerdot 
Text shortened.



@3313

8 years 
tranquil 
redrawn fork flow in tikz, adding the cost plugin



@3312

8 years 
sacerdot 
…



@3311

8 years 
sacerdot 
…



@3310

8 years 
sacerdot 
An example.



@3309

8 years 
sacerdot 
An abstract.



@3308

8 years 
sacerdot 
Authors and affiliations



@3307

8 years 
sacerdot 
Importing text from D1.4.



@3306

8 years 
tranquil 
altre modifiche e qualche taglio (i risultati per tll e tal)



@3305

8 years 
tranquil 
messo qualche figura, e molte notazioni



@3304

8 years 
boender 
 added 2012 reviews
 updated affiliation



@3303

8 years 
amadio 
r



@3302

8 years 
mckinna 
removed local verison for JHM's machine wp6.tex definitive



@3301

8 years 
mckinna 
updates: wp6.tex is definitive



@3300

8 years 
mckinna 
updates



@3299

8 years 
sacerdot 
…



@3298

8 years 
sacerdot 
…



@3297

8 years 
tranquil 
final version



@3296

8 years 
sacerdot 
…



@3295

8 years 
sacerdot 
…



@3294

8 years 
mckinna 
draft final version: more to say than to put on slides etc.



@3293

8 years 
mckinna 
more: desitination data (partial)



@3292

8 years 
mckinna 
update



@3291

8 years 
mckinna 
template beamer file, and notes for the talk
more later today!



@3290

8 years 
Ian Stark 
Minor edits to slides



@3289

8 years 
sacerdot 
…



@3288

8 years 
sacerdot 
The deliverables resubmitted during the third period.



@3287

8 years 
tranquil 
backend slides



@3286

8 years 
Ian Stark 
Renaming and moving



@3285

8 years 
Ian Stark 
Renaming and moving



@3284

8 years 
Ian Stark 
Moving and renaming



@3283

8 years 
regisgia 
* Compiled version.



@3282

8 years 
regisgia 
* WP5 slides for the final review.



@3281

8 years 
tranquil 
back end correctness slides, alas still incomplete



@3280

8 years 
Ian Stark 
Front end final review talk?



@3279

8 years 
Ian Stark 
Renaming and moving



@3278

8 years 
Ian Stark 
Renaming and moving



@3277

8 years 
Ian Stark 
Renaming and moving



@3276

8 years 
Ian Stark 
Renaming and moving



@3275

8 years 
Ian Stark 
Renaming and moving



@3274

8 years 
Ian Stark 
Rnaming and moving



@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 frontend 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 frontend 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 frontend 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.46.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 
acctrusted 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 cercoexecutable 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.


