# Changeset 3461 for Papers

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

more fiddling

File:
1 edited

### Legend:

Unmodified
 r3460 obtained using invariant generators, tools to produce proof obligations from generated invariants and automatic theorem provers to verify the obligations. If the automatic provers are able to generate proof traces that can be these tools are able to generate proof traces that can be independently checked, the only remaining component that enters the trusted code base is an off-the-shelf invariant generator which, in turn, can be proved \end{tikzpicture} \end{tabular} \caption{On the left: code to count the array's elements that are less than or equal to the threshold. On the right: CerCo's interaction diagram. CerCo's components are drawn solid.} \caption{On the left: C code to count the number of elements in an array that are less than or equal to a given threshold. On the right: CerCo's interaction diagram. Components provided by CerCo are drawn with a solid border.} \label{test1} \end{figure} Twelve proof obligations are generated from~\autoref{itest1} (to prove that the loop invariant holds after one execution if it holds before, to prove that the whole program execution takes at most 1358 cycles, etc.).  Note that the synthesised time bound for \lstinline'count', to prove that the whole program execution takes at most 1358 cycles, and so on).  Note that the synthesised time bound for \lstinline'count', $178+214*(1+\text{\lstinline'len'})$ cycles, is parametric in the length of the array. The CVC3 prover soundness does not depend on the cost plugin, which can in principle produce any synthetic cost. However, in order to be able to actually prove a WCET of a C function, we need to add correct annotations in a way that prove the WCET of a C function, we need to add correct annotations in a way that Jessie and subsequent automatic provers have enough information to deduce their validity. In practice this is not straightforward even for very simple programs The cost annotations added by the CerCo compiler take the form of C instructions that update a fresh global variable called the cost variable by a constant. Synthesizing a WCET of a C function thus consists of statically resolving an Synthesizing the WCET of a C function thus consists of statically resolving an upper bound of the difference between the value of the cost variable before and after the execution of the function, i.e. finding the instructions