source: Deliverables/Dissemination/README @ 2567

Last change on this file since 2567 was 2567, checked in by amadio, 9 years ago


File size: 2.8 KB
2This directory contains documents for the presentation of the project
3in the dissemination workshops and in the final review.
5Each module is supposed to last between 15' and 30', so it should be
6supported by a set of 15-30 slides and possibly by a short demo.
8Not all modules need to be presented each time.
12Abstract (*To come (Bologna?)*)
15The labelling approach to certified cost annotations.
17We present a so-called labelling method to enrich a compiler in order
18to turn it into a ``cost annotating compiler'', that is, a compiler
19which can ``lift'' pieces of information on the execution cost of the
20object code as cost annotations on the source code. These cost
21annotations characterize the execution costs of code fragments of
22constant complexity.  First, we provide a proof methodology that
23extends standard simulation proofs of compiler correctness to ensure
24that the cost annotations on the source code are sound and precise
25with respect to an execution cost model of the object code.  Second,
26we demonstrate that our label-based instrumentation is scalable
27because it consists in a modular extension of the compilation
28chain. To that end, we report our successful experience in
29implementing and testing the labelling approach on top of a prototype
30compiler written in OCAML for (a large fragment of) the C language.
33Reasoning on cost annotations of C programms.
35We provide evidence for the usability of the generated cost
36annotations as a mean to reason on the concrete complexity of programs
37written in C. For this purpose, we present a Frama-C plugin that uses
38our cost annotating compiler to automatically infer trustworthy logic
39assertions about the concrete worst case execution cost of programs
40written in a fragment of the C language. These logic assertions are
41synthetic in the sense that they characterize the cost of executing
42the entire program, not only constant-time fragments. (These bounds
43may depend on the size of the input data.) We report our
44experimentations on some C programs, including programs generated by a
45compiler for the synchronous programming language Lustre used in
46critical embedded software.
50Targeting more advanced optimisations: indexed labelling (tentative title).
51Abstract (* To come (Bologna?)*)
54Certifying and reasoning on cost annotations of functional programs.
56We design a labelling method to insert cost annotations in a
57higher-order functional program, to certify their correctness with
58respect to a standard, typable compilation chain to assembly code
59including safe memory management, and to reason about them in a
60higher-order Hoare logic.
61Slides: funcca-slide.pdf
64Compiler certification in Matita (tentative title, add more modules if needed...)
65Abstract (*To come (Edinburgh/Bologna?)*)
Note: See TracBrowser for help on using the repository browser.