Changeset 3427 for Papers


Ignore:
Timestamp:
Feb 11, 2014, 6:41:19 PM (6 years ago)
Author:
campbell
Message:

Make example clearer for readers in black and white.

Location:
Papers/fopara2013
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/appendix.tex

    r3426 r3427  
    99Section 2 has been restructured to give a clearer comparison of
    1010existing approaches with CerCo.
     11
     12Section 4 has been reorganised to highlight the connections between
     13the different parts of the work.
     14
     15The citation of a survey of state-of-the-art WCET tools has been made
     16more explicit as a source of information about tools such as AbsInt.
  • Papers/fopara2013/fopara13.tex

    r3426 r3427  
    435435\label{test1}
    436436\end{figure}
    437 We illustrate the workflow we envisage (on the right of~\autoref{test1})
    438 on an example program (on the left of~\autoref{test1}).
    439 The user writes the program and feeds it to the CerCo compiler, which outputs
    440 an instrumented version of the same program that updates global variables
    441 that record the elapsed execution time and the stack space usage.
    442 The red lines in \autoref{itest1} are the instrumentation introduced by the
    443 compiler. The annotated program can then be enriched with complexity assertions
    444 in the style of Hoare logic, that are passed to a deductive platform (in our
    445 case Frama-C). We provide as a Frama-C cost plugin a simple automatic
    446 synthesiser for complexity assertions (the blue lines in \autoref{itest1}),
    447 which can be overridden by the user to increase or decrease accuracy. From the
    448 assertions, a general purpose deductive platform produces proof obligations
    449 which in turn can be closed by automatic or interactive provers, ending in a
    450 proof certificate.
     437We illustrate the workflow we envisage (on the right
     438of~\autoref{test1}) on an example program (on the left
     439of~\autoref{test1}).  The user writes the program and feeds it to the
     440CerCo compiler, which outputs an instrumented version of the same
     441program that updates global variables that record the elapsed
     442execution time and the stack space usage.  The red lines in
     443\autoref{itest1} introducing variables, functions and function calls
     444starting \lstinline'__cost' and \lstinline'__stack' are the instrumentation introduced by the
     445compiler.
     446
     447 The annotated program can then be enriched with complexity
     448assertions in the style of Hoare logic, that are passed to a deductive
     449platform (in our case Frama-C). We provide as a Frama-C cost plugin a
     450simple automatic synthesiser for complexity assertions (the blue
     451comments starting with \lstinline'/*@' in \autoref{itest1}), which can
     452be overridden by the user to increase or decrease accuracy. From the
     453assertions, a general purpose deductive platform produces proof
     454obligations which in turn can be closed by automatic or interactive
     455provers, ending in a proof certificate.
    451456
    452457% NB: if you try this example with the live CD you should increase the timeout
Note: See TracChangeset for help on using the changeset viewer.