Changeset 3290

Timestamp:

May 15, 2013, 2:24:30 AM (7 years ago)

Author:

Ian Stark

Message:

Minor edits to slides

Location:

Deliverables/Dissemination/final-review/wp3

Files:

• front-end.pdf (added)
• front-end.tex (modified) (4 diffs)

Deliverables/Dissemination/final-review/wp3/front-end.tex

@@ -128 +128 @@
   \item Labelling and compilation of source through these;
   \item Innovation of \red{structured traces}, originally to support timing
-    computation in the assembler.
+    calculation in the assembler.
   \end{itemize}
 
@@ -197 +197 @@
   \item From a language with explicit call/return structure and high-level
     structured control flow;
-  \item To a language where all control flow is unconstrained jumps.
+  \item To a language with unconstrained jumps for control flow.
   \end{itemize}
 
@@ -380 +380 @@
   This check of soundness and precision in RTLabs:
   \begin{itemize}
-  \item Is partial --- will only succeed when invariants hold;
+  \item Will always succeed when invariants hold (and fail when not);
   \item Extracts to additional checking code in the compiler;
   \item[\checkmark] Significantly reduces the proof effort.
@@ -394 +394 @@
     finite bound on the number of instructions until the next cost label.
   \end{quote}
-  We expect that proving existence in general of this bound alone to be
-  considerably harder than the whole check.
+  We expect just proving existence of this bound to be considerably harder
+  than implementing the whole checking mechanism.
 
 \end{frame}