Changeset 3290
- Timestamp:
- May 15, 2013, 2:24:30 AM (7 years ago)
- Location:
- Deliverables/Dissemination/final-review/wp3
- Files:
-
- 1 added
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/Dissemination/final-review/wp3/front-end.tex
r3280 r3290 128 128 \item Labelling and compilation of source through these; 129 129 \item Innovation of \red{structured traces}, originally to support timing 130 c omputation in the assembler.130 calculation in the assembler. 131 131 \end{itemize} 132 132 … … 197 197 \item From a language with explicit call/return structure and high-level 198 198 structured control flow; 199 \item To a language w here all control flow is unconstrained jumps.199 \item To a language with unconstrained jumps for control flow. 200 200 \end{itemize} 201 201 … … 380 380 This check of soundness and precision in RTLabs: 381 381 \begin{itemize} 382 \item Is partial --- will only succeed when invariants hold;382 \item Will always succeed when invariants hold (and fail when not); 383 383 \item Extracts to additional checking code in the compiler; 384 384 \item[\checkmark] Significantly reduces the proof effort. … … 394 394 finite bound on the number of instructions until the next cost label. 395 395 \end{quote} 396 We expect that proving existence in general of this bound alone to be397 considerably harder than the whole check.396 We expect just proving existence of this bound to be considerably harder 397 than implementing the whole checking mechanism. 398 398 399 399 \end{frame}
Note: See TracChangeset
for help on using the changeset viewer.