| author | Christian Urban <urbanc@in.tum.de> | 
| Tue, 27 Nov 2018 00:45:26 +0000 | |
| changeset 609 | ff17a6f694dd | 
| parent 538 | e03107e79d26 | 
| child 610 | ce5e0426c92a | 
| permissions | -rw-r--r-- | 
| 65 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 1 | \documentclass[dvipsnames,14pt,t]{beamer}
 | 
| 309 
640e4a05cd9b
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 2 | \usepackage{../slides}
 | 
| 215 
828303e8e4af
updated slides
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
207diff
changeset | 3 | \usepackage{../langs}
 | 
| 609 | 4 | \usepackage{../data}
 | 
| 309 
640e4a05cd9b
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 5 | \usepackage{../graphics}
 | 
| 379 
fa2589ec0fae
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
312diff
changeset | 6 | \usepackage{../grammar}
 | 
| 310 
d384fe01d0e8
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
309diff
changeset | 7 | \usepackage{soul}
 | 
| 609 | 8 | |
| 310 
d384fe01d0e8
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
309diff
changeset | 9 | |
| 609 | 10 | % beamer stuff | 
| 459 | 11 | \renewcommand{\slidecaption}{CFL 09, King's College London}
 | 
| 609 | 12 | \newcommand{\bl}[1]{\textcolor{blue}{#1}}       
 | 
| 13 | ||
| 310 
d384fe01d0e8
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
309diff
changeset | 14 | |
| 65 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 15 | \begin{document}
 | 
| 609 | 16 | |
| 65 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 17 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 309 
640e4a05cd9b
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
215diff
changeset | 18 | \begin{frame}[t]
 | 
| 65 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 19 | \frametitle{%
 | 
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 20 |   \begin{tabular}{@ {}c@ {}}
 | 
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 21 | \\[-3mm] | 
| 459 | 22 | \LARGE Compilers and \\[-2mm] | 
| 538 | 23 | \LARGE Formal Languages (9)\\[3mm] | 
| 65 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 24 |   \end{tabular}}
 | 
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 25 | |
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 26 | \normalsize | 
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 27 |   \begin{center}
 | 
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 28 |   \begin{tabular}{ll}
 | 
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 29 | Email: & christian.urban at kcl.ac.uk\\ | 
| 609 | 30 |   Office: & N\liningnums{7.07} (North Wing, Bush House)\\
 | 
| 31 | Slides: & KEATS (also homework is there)\\ | |
| 538 | 32 |   \end{tabular}
 | 
| 33 |   \end{center}
 | |
| 310 
d384fe01d0e8
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
309diff
changeset | 34 | |
| 609 | 35 | \end{frame}
 | 
| 36 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 37 | ||
| 38 | ||
| 39 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 40 | \begin{frame}[t]
 | |
| 41 | \frametitle{While Language}
 | |
| 42 | ||
| 43 | \begin{center}
 | |
| 44 | \bl{\begin{tabular}{@{}lcl@{}}
 | |
| 45 | \\[-12mm] | |
| 46 | \meta{Stmt} & $::=$ &  $\texttt{skip}$\\
 | |
| 47 |               & $|$ & \textit{Id}\;\texttt{:=}\;\meta{AExp}\\
 | |
| 48 |               & $|$ & \texttt{if}\; \meta{BExp} \;\texttt{then}\; \meta{Block} \;\texttt{else}\; \meta{Block}\\
 | |
| 49 |               & $|$ & \texttt{while}\; \meta{BExp} \;\texttt{do}\; \meta{Block}\\
 | |
| 50 |               & $|$ & \texttt{read}\;\textit{Id}\\
 | |
| 51 |               & $|$ & \texttt{write}\;\textit{Id}\\
 | |
| 52 |               & $|$ & \texttt{write}\;\textit{String}\medskip\\
 | |
| 53 | \meta{Stmts} & $::=$ &  \meta{Stmt} \;\texttt{;}\; \meta{Stmts} $|$  \meta{Stmt}\medskip\\
 | |
| 54 | \meta{Block} & $::=$ &  \texttt{\{}\,\meta{Stmts}\,\texttt{\}} $|$ \meta{Stmt}\medskip\\
 | |
| 55 | \meta{AExp} & $::=$ & \ldots\\
 | |
| 56 | \meta{BExp} & $::=$ & \ldots\\
 | |
| 57 | \end{tabular}}
 | |
| 58 | \end{center}
 | |
| 59 | \end{frame}
 | |
| 60 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 61 | ||
| 62 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 63 | \begin{frame}[c]
 | |
| 64 | \frametitle{\begin{tabular}{c}Fibonacci Numbers\end{tabular}}
 | |
| 65 | ||
| 66 | \mbox{}\\[-18mm]\mbox{}
 | |
| 67 | ||
| 68 | {\lstset{language=While}\fontsize{10}{12}\selectfont
 | |
| 69 | \texttt{\lstinputlisting{../progs/fib.while}}}
 | |
| 70 | ||
| 71 | \end{frame}
 | |
| 72 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 73 | ||
| 74 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 75 | \begin{frame}[c,fragile]
 | |
| 76 | \frametitle{BF***}
 | |
| 77 | ||
| 78 | some big array, say \texttt{a}; 7 (8) instructions:
 | |
| 79 | ||
| 80 | \begin{itemize}
 | |
| 81 | \item \texttt{>} move \texttt{ptr++}
 | |
| 82 | \item \texttt{<} move \texttt{ptr-{}-}
 | |
| 83 | \item \texttt{+} add \texttt{a[ptr]++}
 | |
| 84 | \item \texttt{-} subtract \texttt{a[ptr]-{}-}
 | |
| 85 | \item \texttt{.} print out \texttt{a[ptr]} as ASCII
 | |
| 86 | \item \texttt{[} if \texttt{a[ptr] == 0} jump just after the corresponding \texttt{]}; otherwise \texttt{ptr++}
 | |
| 87 | \item \texttt{]} if \texttt{a[ptr] != 0} jump just after the corresponding \texttt{[}; otherwise \texttt{ptr++}
 | |
| 88 | ||
| 89 | \end{itemize}  
 | |
| 90 | ||
| 91 | \end{frame}
 | |
| 92 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 93 | ||
| 94 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 95 | \begin{frame}[c,fragile]
 | |
| 96 | \frametitle{Arrays in While}
 | |
| 310 
d384fe01d0e8
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
309diff
changeset | 97 | |
| 609 | 98 | \begin{itemize}
 | 
| 99 | \item \texttt{new arr[15000]}\medskip 
 | |
| 100 | \item \texttt{x := 3 + arr[3 + y]}\medskip 
 | |
| 101 | \item \texttt{arr[42 * n] := ...}
 | |
| 102 | \end{itemize}  
 | |
| 103 | ||
| 104 | \end{frame}
 | |
| 105 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 106 | ||
| 107 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 108 | \begin{frame}[c,fragile]
 | |
| 109 | \frametitle{New Arrays}
 | |
| 110 | ||
| 111 | \begin{lstlisting}[mathescape,numbers=none,language=While]
 | |
| 112 | new arr[number] | |
| 113 | \end{lstlisting}\bigskip\bigskip
 | |
| 114 | ||
| 115 | \begin{lstlisting}[mathescape,numbers=none,language=While]
 | |
| 116 | ldc number | |
| 117 | newarray int | |
| 118 | astore loc_var | |
| 119 | \end{lstlisting}
 | |
| 120 | ||
| 121 | ||
| 122 | \end{frame}
 | |
| 123 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 124 | ||
| 125 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 126 | \begin{frame}[c,fragile]
 | |
| 127 | \frametitle{Array Update}
 | |
| 128 | ||
| 129 | \begin{lstlisting}[mathescape,numbers=none,language=While]
 | |
| 130 | arr[...] := | |
| 131 | \end{lstlisting}\bigskip\bigskip
 | |
| 132 | ||
| 133 | \begin{lstlisting}[mathescape,numbers=none,language=While]
 | |
| 134 | aload loc_var | |
| 135 | index_aexp | |
| 136 | value_aexp | |
| 137 | iastore | |
| 138 | \end{lstlisting}
 | |
| 139 | ||
| 140 | ||
| 141 | \end{frame}
 | |
| 142 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 143 | ||
| 144 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 145 | \begin{frame}[c,fragile]
 | |
| 146 | \frametitle{Array Lookup in AExp}
 | |
| 147 | ||
| 148 | \begin{lstlisting}[mathescape,numbers=none,language=While]
 | |
| 149 | ...arr[...]... | |
| 150 | \end{lstlisting}\bigskip\bigskip
 | |
| 151 | ||
| 152 | \begin{lstlisting}[mathescape,numbers=none,language=While]
 | |
| 153 | aload loc_var | |
| 154 | index_aexp | |
| 155 | iaload | |
| 156 | \end{lstlisting}
 | |
| 157 | ||
| 158 | ||
| 159 | \end{frame}
 | |
| 160 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 310 
d384fe01d0e8
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
309diff
changeset | 161 | |
| 
d384fe01d0e8
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
309diff
changeset | 162 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 163 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 164 |   \begin{frame}[c]
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 165 |   \frametitle{Dijkstra on Testing}
 | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 166 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 167 |   \begin{bubble}[10cm]
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 168 | ``Program testing can be a very effective way to show the | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 169 | presence of bugs, but it is hopelessly inadequate for showing | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 170 | their absence.'' | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 171 |   \end{bubble}\bigskip
 | 
| 609 | 172 | |
| 173 | \small | |
| 174 | What is good about compilers: the either seem to work, | |
| 175 | or go horribly wrong (most of the time). | |
| 176 | ||
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 177 |   \end{frame}
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 178 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 179 | |
| 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 180 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 181 | \begin{frame}[c]
 | 
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 182 | \frametitle{\Large Proving Programs to be Correct}
 | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 183 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 184 | \begin{bubble}[10cm]
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 185 | \small | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 186 | {\bf Theorem:} There are infinitely many prime 
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 187 | numbers.\medskip\\ | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 188 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 189 | {\bf Proof} \ldots\\
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 190 | \end{bubble}\bigskip
 | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 191 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 192 | |
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 193 | similarly\bigskip | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 194 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 195 | \begin{bubble}[10cm]
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 196 | \small | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 197 | {\bf Theorem:} The program is doing what 
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 198 | it is supposed to be doing.\medskip | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 199 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 200 | {\bf Long, long proof} \ldots\\
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 201 | \end{bubble}\bigskip\medskip
 | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 202 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 203 | \small This can be a gigantic proof. The only hope is to have | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 204 | help from the computer. `Program' is here to be understood to be | 
| 609 | 205 | quite general (compiler, OS, \ldots). | 
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 206 | |
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 207 | \end{frame}
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 208 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 209 | |
| 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 210 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 211 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 212 | |
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 213 | \begin{frame}[c]
 | 
| 609 | 214 | \frametitle{Can This Be Done?}
 | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 215 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 216 | \begin{itemize}
 | 
| 609 | 217 | \item in 2008, verification of a small C-compiler | 
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 218 | \begin{itemize}
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 219 | \item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour'' | 
| 609 | 220 | \item is as good as \texttt{gcc -O1}, but much, much less buggy 
 | 
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 221 | \end{itemize}
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 222 | \end{itemize}
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 223 | |
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 224 | \begin{center}
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 225 |   \includegraphics[scale=0.12]{../pics/compcert.png}
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 226 | \end{center}
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 227 | |
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 228 | \end{frame}
 | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 229 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 230 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 231 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 232 | \begin{frame}[c]
 | 
| 609 | 233 | \frametitle{Fuzzy Testing C-Compilers}
 | 
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 234 | |
| 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 235 | \begin{itemize}
 | 
| 609 | 236 | \item tested GCC, LLVM and others by randomly generating | 
| 237 | C-programs | |
| 238 | \item found more than 300 bugs in GCC and also | |
| 239 | many in LLVM (some of them highest-level critical)\bigskip | |
| 240 | \item about CompCert: | |
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 241 | |
| 609 | 242 | \begin{bubble}[10cm]\small ``The striking thing about our CompCert
 | 
| 243 | results is that the middle-end bugs we found in all other | |
| 244 | compilers are absent. As of early 2011, the under-development | |
| 245 | version of CompCert is the only compiler we have tested for | |
| 246 | which Csmith cannot find wrong-code errors. This is not for | |
| 247 | lack of trying: we have devoted about six CPU-years to the | |
| 248 | task.'' | |
| 249 | \end{bubble} 
 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 250 | \end{itemize}
 | 
| 206 
85b961f1eee9
added
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
151diff
changeset | 251 | |
| 383 
a6a6bf32fade
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
381diff
changeset | 252 | \end{frame}
 | 
| 609 | 253 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | 
| 82 
06c3ec0b452e
updated
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 
81diff
changeset | 254 | |
| 65 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 255 | \end{document}
 | 
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 256 | |
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 257 | %%% Local Variables: | 
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 258 | %%% mode: latex | 
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 259 | %%% TeX-master: t | 
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 260 | %%% End: | 
| 
ade6af51402c
tuned
 Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff
changeset | 261 |