# HG changeset patch
# User wu
# Date 1344854257 0
# Node ID c89f82fb95f8b9ab25c1cd456c6d6acb54a765ba
# Parent  e089ed1c3e2669bf2a193d16bcafe747ed916d5b
Slightly modifications.

diff -r e089ed1c3e26 -r c89f82fb95f8 prio/Slides/Slides1.thy
--- a/prio/Slides/Slides1.thy	Fri Aug 10 13:57:41 2012 +0000
+++ b/prio/Slides/Slides1.thy	Mon Aug 13 10:37:37 2012 +0000
@@ -38,7 +38,7 @@
 
 
 text_raw {*
-  \renewcommand{\slidecaption}{London, 28 June 2012}
+  \renewcommand{\slidecaption}{Nanjing, P.R. China, 1 August 2012}
   \newcommand{\bl}[1]{#1}                        
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -75,10 +75,10 @@
   \frametitle{\large Prioirty Inheritance Protocol (PIP)}
   \large
 
-  \begin{itemize} \large
+  \begin{itemize} 
   \item Widely used in Real-Time OSs \pause
-  \item One solution of \textcolor{red}{`Priority Inversion'} problem \pause
-  \item A flawed manual correctness proof (1990) \pause
+  \item One solution of \textcolor{red}{`Priority Inversion'} \pause
+  \item A flawed manual correctness proof (1990)\pause
         \begin{itemize} \large
           \item {Notations with no precise definition}
           \item {Resorts to intuitions}
@@ -88,7 +88,7 @@
           \item {Applicable to small size system models}
           \item { Unhelpful for human understanding } 
         \end{itemize} \pause
-  \item Verification of PCP in PVS (2000) \pause
+  \item Verification of PCP in PVS (2000)\pause
         \begin{itemize} \large
            \item {A related protocol}
            \item {Priority Ceiling Protocol}
@@ -350,7 +350,7 @@
   \pause
 
   \begin{center}
-  \includegraphics[scale=0.45]{EventAbstract.png}
+  \includegraphics[scale=0.4]{EventAbstract.png}
   \end{center}
 
   \end{frame}}
@@ -519,7 +519,6 @@
   \pause
   \small
   $^\star$ modulo some further assumptions\bigskip\pause
-
   It does not matter which process gets a released lock.
 
   \end{frame}}
@@ -633,15 +632,15 @@
   \begin{itemize} \large
   \item Aims fulfilled \medskip \pause
   \item Alternative way \pause
-       \begin{itemize}
+       \begin{itemize} 
            \item using Isabelle/HOL in OS code development \medskip
            \item through the Inductive Approach
        \end{itemize} \pause
   \item Future researches \pause
-       \begin{itemize} \large
+       \begin{itemize}
            \item scheduler in RT-Linux\medskip
            \item multiprocessor case\medskip
-           \item other ``nails'' ? (networks, \ldots) \pause
+           \item other ``nails'' ? (networks, \ldots) \medskip \pause
            \item Refinement to real code and relation between implemenations
         \end{itemize}
   \end{itemize}
@@ -649,6 +648,20 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Questions?}
+  
+  \begin{itemize} \large
+  \item Thank you for listening!
+  \end{itemize}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
 
 (*<*)
 end
diff -r e089ed1c3e26 -r c89f82fb95f8 prio/Slides/slides.pdf
Binary file prio/Slides/slides.pdf has changed