Changeset 3290


Ignore:
Timestamp:
May 15, 2013, 2:24:30 AM (4 years ago)
Author:
stark
Message:

Minor edits to slides

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  
    128128  \item Labelling and compilation of source through these;
    129129  \item Innovation of \red{structured traces}, originally to support timing
    130     computation in the assembler.
     130    calculation in the assembler.
    131131  \end{itemize}
    132132
     
    197197  \item From a language with explicit call/return structure and high-level
    198198    structured control flow;
    199   \item To a language where all control flow is unconstrained jumps.
     199  \item To a language with unconstrained jumps for control flow.
    200200  \end{itemize}
    201201
     
    380380  This check of soundness and precision in RTLabs:
    381381  \begin{itemize}
    382   \item Is partial --- will only succeed when invariants hold;
     382  \item Will always succeed when invariants hold (and fail when not);
    383383  \item Extracts to additional checking code in the compiler;
    384384  \item[\checkmark] Significantly reduces the proof effort.
     
    394394    finite bound on the number of instructions until the next cost label.
    395395  \end{quote}
    396   We expect that proving existence in general of this bound alone to be
    397   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.
    398398
    399399\end{frame}
Note: See TracChangeset for help on using the changeset viewer.