 Timestamp:
 Feb 21, 2014, 11:50:26 AM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/fopara2013/fopara13.tex
r3460 r3461 330 330 obtained using invariant generators, tools to produce proof obligations from 331 331 generated invariants and automatic theorem provers to verify the obligations. If 332 the automatic provers are able to generate proof traces that can be332 these tools are able to generate proof traces that can be 333 333 independently checked, the only remaining component that enters the trusted code 334 334 base is an offtheshelf invariant generator which, in turn, can be proved … … 441 441 \end{tikzpicture} 442 442 \end{tabular} 443 \caption{On the left: code to count the array's elements444 that are less than or equal to thethreshold. On the right: CerCo's interaction445 diagram. C erCo's components are drawn solid.}443 \caption{On the left: C code to count the number of elements in an array 444 that are less than or equal to a given threshold. On the right: CerCo's interaction 445 diagram. Components provided by CerCo are drawn with a solid border.} 446 446 \label{test1} 447 447 \end{figure} … … 474 474 Twelve proof obligations are generated from~\autoref{itest1} (to prove 475 475 that the loop invariant holds after one execution if it holds before, 476 to prove that the whole program execution takes at most 1358 cycles, 477 etc.). Note that the synthesised time bound for \lstinline'count', 476 to prove that the whole program execution takes at most 1358 cycles, and so on). Note that the synthesised time bound for \lstinline'count', 478 477 $178+214*(1+\text{\lstinline'len'})$ cycles, is parametric in the length of 479 478 the array. The CVC3 prover … … 1009 1008 soundness does not depend on the cost plugin, which can in 1010 1009 principle produce any synthetic cost. However, in order to be able to actually 1011 prove aWCET of a C function, we need to add correct annotations in a way that1010 prove the WCET of a C function, we need to add correct annotations in a way that 1012 1011 Jessie and subsequent automatic provers have enough information to deduce their 1013 1012 validity. In practice this is not straightforward even for very simple programs … … 1029 1028 The cost annotations added by the CerCo compiler take the form of C instructions 1030 1029 that update a fresh global variable called the cost variable by a constant. 1031 Synthesizing aWCET of a C function thus consists of statically resolving an1030 Synthesizing the WCET of a C function thus consists of statically resolving an 1032 1031 upper bound of the difference between the value of the cost variable before and 1033 1032 after the execution of the function, i.e. finding the instructions
Note: See TracChangeset
for help on using the changeset viewer.