The draft will be updated a few times to improve the presentation of the final version. When I update it, I will include a summary of the changes that went into the new version.
Draft of July 20th: Complete rewrite of the related work. Lots of typographical and minor error fixes in Chapter 2 together with three new explanatory paragraphs. Added acknowledgements.
Draft of July 13th: Two additional paragraphs in Chapter 3. New experimental evaluations in Chapters 3 and 4. Misc typo fixes.
Draft of July 3rd: Initial revision.
Invariant logics of Chapter 2: InvariantLogic.v
Translation proofs for the stack quantitative logic of Chapter 3: LogicMorphisms1.v
Quantitative CompCert of Chapter 3: veristack.zip Also contains the implementation of the quantitative logic given to the AEC of PLDI'14.
Translation proof for tick quantitative logic of Chapter 4: LogicMorphisms2.v
Coq support library for the bound certificates of Chapter 6: pastis-coq.zip