

@3453

6 years 
mulligan 
reworking up to Section 2



@3452

6 years 
mulligan 
changes to second para



@3451

6 years 
mulligan 
deTristram Shandefied the opening paragraph



@3450

6 years 
mulligan 
small rewordings of the abstract, working on rest of paper



@3449

6 years 
piccolo 
clean up



@3448

6 years 
piccolo 



@3447

6 years 
piccolo 
correctness proof in place



@3446

6 years 
piccolo 
Correctness proof, closed all cases except the big lemma one



@3445

6 years 
piccolo 
correctness proof finished with a big open lemma



@3444

6 years 
mulligan 
More language changes. At end of file.



@3443

6 years 
mulligan 
More changes, including more missing references (including to CerCo?'s …



@3442

6 years 
mulligan 
Changes up to Section 3. Added missing reference to AbsInt?'s aiT tools.



@3441

6 years 
mulligan 
Some language/spelling changes in fopara2013.tex up to Section 2. …



@3440

6 years 
campbell 
Add a preformatted PDF.



@3439

6 years 
campbell 
Fiddle references back into one page.



@3438

6 years 
campbell 
Appendix about the reviewer's comments.



@3437

6 years 
campbell 
Deal more directly with some reviewer's comments.



@3436

6 years 
campbell 
Section 4.5 revisions.



@3435

6 years 
campbell 
Revise section 4.4.



@3434

6 years 
campbell 
Section 4.3 revised.



@3433

6 years 
campbell 
Revise sections 4.1, 4.2.



@3432

6 years 
campbell 
Consistently use ll spelling of labelled/labelling.



@3431

6 years 
campbell 
Note the specification language in Sec 3.



@3430

6 years 
campbell 
Revisions up to the end of section 3.



@3429

6 years 
campbell 
Adjust figure formatting to fit in page without being unreadable.



@3428

6 years 
campbell 
More minor stuff.



@3427

6 years 
campbell 
Make example clearer for readers in black and white.



@3426

6 years 
campbell 
Clarify WCET stateoftheart citation.



@3425

6 years 
campbell 
Rearrange section 4



@3424

6 years 
campbell 
Minor edits to section 4.



@3423

6 years 
campbell 
Note for appendix.



@3422

6 years 
campbell 
Basic restructuring of section 2.



@3421

6 years 
campbell 
Note parametric example for appendix



@3420

6 years 
campbell 
Parametric example for FOPARA.



@3419

6 years 
campbell 
Tweak abstract.



@3418

6 years 
campbell 
Move preproceedings version of FOPARA paper aside.



@3417

6 years 
campbell 
Many of the minor reviewer comments about FOPARA paper.



@3416

6 years 
piccolo 



@3415

6 years 
boender 
 changes for proceedings of TACAS 2014



@3414

6 years 
piccolo 



@3413

6 years 
sacerdot 
…



@3412

6 years 
sacerdot 
…



@3411

6 years 
piccolo 
new statement of correctness theorem in place



@3410

6 years 
piccolo 
we just realized that correctness theorem is wrong in the way it is …



@3409

6 years 
piccolo 



@3408

6 years 
piccolo 



@3407

6 years 
sacerdot 
Added get_element_append_r1.



@3406

6 years 
piccolo 



@3405

6 years 
piccolo 
closed some daemons



@3404

6 years 
piccolo 



@3403

6 years 
piccolo 



@3402

6 years 
piccolo 



@3401

6 years 
sacerdot 
More goals closed, but some are false.



@3400

6 years 
piccolo 



@3399

6 years 
piccolo 
call case not absorbing



@3398

6 years 
piccolo 
state relation with stack relation uptaded



@3397

6 years 
piccolo 
partial commit



@3396

6 years 
piccolo 
correctness proof in developping



@3395

6 years 
fguidi 
scan for redundant includes with new version of matitadep



@3394

6 years 
piccolo 
Added abstract language and procedure to add call post labelled



@3393

6 years 
boender 
 TACAS stuff



@3392

6 years 
boender 
 renamed paper yet again



@3391

6 years 
piccolo 
Definition of well formed trace is in the operational semantics



@3390

6 years 
piccolo 
Patched simulation proof, changed definition of silent trace



@3389

6 years 
piccolo 
Ended simulation proof



@3388

6 years 
piccolo 
partial commit



@3387

7 years 
piccolo 
unified notation



@3386

7 years 
sacerdot 
Something that seems to be working after all.



@3385

7 years 
sacerdot 
…



@3384

7 years 
sacerdot 
Bug found?? We think so.



@3383

7 years 
sacerdot 
Simple simulation conditions and statements added.
The complex ones …



@3382

7 years 
sacerdot 
The simulation statement.



@3381

7 years 
sacerdot 
Pen&paper style hypotheses and statements for the staticdynamic …



@3380

7 years 
piccolo 
Added definition of measurable trace



@3379

7 years 
sacerdot 
Semantics completed.



@3378

7 years 
sacerdot 
 Stuff common to both languages is now in Common.ma
 object …



@3377

7 years 
sacerdot 
 emit l removed
+ io l1 l2
The semantics has been changed so that …



@3376

7 years 
sacerdot 
Semantics fixed: the value of the anonymous variable was corrupted by …



@3375

7 years 
sacerdot 
Imp language and its labelledSOS.
 The language has function calls …



@3374

7 years 
piccolo 



@3373

7 years 
sacerdot 
…



@3372

7 years 
piccolo 
Added new implementation of labelling approach based on LTS and …



@3371

7 years 
piccolo 
Modified RTLsemantics and ERTLsemantics. Now the pop frame will set …



@3370

7 years 
sacerdot 
Submitted.



@3369

7 years 
sacerdot 
submitted



@3368

7 years 
sacerdot 
..



@3367

7 years 
tranquil 
…



@3366

7 years 
tranquil 
…



@3365

7 years 
boender 
 changed spelling error



@3364

7 years 
boender 
 added bit to the introduction about contribution



@3363

7 years 
boender 
 renamed directory



@3362

7 years 
boender 
 added some bits as per Claudio's mail
 rewrote some small things
 …



@3361

7 years 
sacerdot 
15 pages version



@3360

7 years 
tranquil 
aggiustate le figure



@3359

7 years 
tranquil 
recuperato un po' della formalizzazione, ancora in fondo.



@3358

7 years 
sacerdot 
…



@3357

7 years 
sacerdot 
…



@3356

7 years 
sacerdot 
…



@3355

7 years 
sacerdot 
…



@3354

7 years 
boender 
 one more


