36 \normalsize |
159 \normalsize |
37 \begin{center} |
160 \begin{center} |
38 \begin{tabular}{ll} |
161 \begin{tabular}{ll} |
39 Email: & christian.urban at kcl.ac.uk\\ |
162 Email: & christian.urban at kcl.ac.uk\\ |
40 %Office: & N\liningnums{7.07} (North Wing, Bush House)\bigskip\\ |
163 %Office: & N\liningnums{7.07} (North Wing, Bush House)\bigskip\\ |
41 Slides \& Code: & KEATS\\ |
164 Slides \& Code: & KEATS\bigskip\\ |
42 % & \onslide<2>{\alert{PDF: A Crash-Course in Scala}}\bigskip\\ |
165 % & \onslide<2>{\alert{PDF: A Crash-Course in Scala}}\bigskip\\ |
43 %Office Hours: & Thursdays 12:00 -- 14:00\\ |
166 %Office Hours: & Thursdays 12:00 -- 14:00\\ |
44 %Additionally: & (for Scala) Tuesdays 10:45 -- 11:45\\ |
167 %Additionally: & (for Scala) Tuesdays 10:45 -- 11:45\\ |
|
168 \multicolumn{2}{c}{\Large\textbf{https://pollev.com/cfltutoratki576}}\\[2cm] |
45 \end{tabular} |
169 \end{tabular} |
46 \end{center} |
170 \end{center} |
47 |
171 |
48 \end{frame} |
172 \end{frame} |
49 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
173 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
174 |
|
175 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
176 \begin{frame}<1>[c] |
|
177 \frametitle{Main 3: Regexes} |
|
178 |
|
179 \begin{center} |
|
180 \mbox{Graphs: regex \alert{\texttt{(a*)*b}} and strings $\underbrace{\;\texttt{a}\ldots \texttt{a}\;}_{n}$}\bigskip |
|
181 |
|
182 |
|
183 \small |
|
184 \begin{tabular}[t]{@{\hspace{-8mm}}c@{\hspace{-0mm}}c@{}} |
|
185 \only<1>{\raisebox{6mm}{\begin{tikzpicture} |
|
186 \begin{axis}[ |
|
187 xlabel={$n$}, |
|
188 x label style={at={(1.05,0.0)}}, |
|
189 ylabel={time in secs}, |
|
190 enlargelimits=false, |
|
191 xtick={0,5,...,30}, |
|
192 xmax=33, |
|
193 ymax=35, |
|
194 ytick={0,5,...,30}, |
|
195 scaled ticks=false, |
|
196 axis lines=left, |
|
197 width=5.5cm, |
|
198 height=5cm, |
|
199 legend entries={Java 8,Python,JavaScript,Swift,Dart}, |
|
200 %legend entries={\small{}Python, \small{}Java 8, \small{}JavaScript}, |
|
201 legend pos=north west, |
|
202 legend cell align=left] |
|
203 \addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data}; |
|
204 \addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data}; |
|
205 \addplot[red,mark=*, mark options={fill=white}] table {re-js.data}; |
|
206 \addplot[magenta,mark=*, mark options={fill=white}] table {re-swift.data}; |
|
207 \addplot[brown,mark=*, mark options={fill=white}] table {re-dart.data}; |
|
208 \end{axis} |
|
209 \end{tikzpicture}}}% |
|
210 \only<2>{\raisebox{0mm}{\begin{tikzpicture} |
|
211 \begin{axis}[ |
|
212 xlabel={$n$}, |
|
213 x label style={at={(1.05,0.0)}}, |
|
214 ylabel={time in secs}, |
|
215 %y label style={at={(0.06,0.5)}}, |
|
216 enlargelimits=false, |
|
217 %xtick={0,30000,...,60000}, |
|
218 xmax=65000, |
|
219 ymax=35, |
|
220 ytick={0,5,...,30}, |
|
221 scaled ticks=true, |
|
222 axis lines=left, |
|
223 width=5.5cm, |
|
224 height=5cm, |
|
225 legend entries={\small{}Java 9}, |
|
226 legend pos=north west] |
|
227 \addplot[cyan,mark=*, mark options={fill=white}] table {re-java9.data}; |
|
228 \end{axis} |
|
229 \end{tikzpicture}}} |
|
230 & |
|
231 \onslide<1-2>{\begin{tikzpicture} |
|
232 \begin{axis}[ |
|
233 xlabel={$n$}, |
|
234 x label style={at={(1.05,0.0)}}, |
|
235 ylabel={time in secs}, |
|
236 enlargelimits=false, |
|
237 ymax=35, |
|
238 ytick={0,5,...,30}, |
|
239 axis lines=left, |
|
240 legend entries={You in M3}, |
|
241 %%scaled ticks=false, |
|
242 width=5.5cm, |
|
243 height=5cm] |
|
244 %%\addplot[green,mark=square*,mark options={fill=white}] table {re2a.data}; |
|
245 \addplot[magenta,mark=square*,mark options={fill=white}] table {re3a.data}; |
|
246 \end{axis} |
|
247 \end{tikzpicture}} |
|
248 \end{tabular} |
|
249 \end{center} |
|
250 |
|
251 \hfill\small\url{https://vimeo.com/112065252} |
|
252 \end{frame} |
|
253 |
|
254 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
255 |
|
256 |
50 |
257 |
51 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
258 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
52 |
259 |
53 %\begin{frame}[c] |
260 %\begin{frame}[c] |
54 %\frametitle{Marks for Preliminary 8} |
261 %\frametitle{Marks for Preliminary 8} |
239 \end{center} |
446 \end{center} |
240 |
447 |
241 \end{frame} |
448 \end{frame} |
242 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
449 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
243 |
450 |
244 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
245 \tikzstyle{sensor}=[draw, fill=blue!20, text width=3.8em, line width=1mm, |
|
246 text centered, minimum height=2em,drop shadow] |
|
247 \tikzstyle{ann} = [above, text width=4em, text centered] |
|
248 \tikzstyle{sc} = [sensor, text width=7em, fill=red!20, |
|
249 minimum height=6em, rounded corners, drop shadow,line width=1mm] |
|
250 |
|
251 \begin{frame}[fragile,c] |
|
252 \frametitle{Compilers 6CCS3CFL} |
|
253 |
|
254 \begin{tikzpicture} |
|
255 % Validation Layer is the same except that there are a set of nodes and links which are added |
|
256 |
|
257 \path (0,0) node (IR) [sc] {\textbf{WHILE Language}\\ compiler}; |
|
258 \path (IR.west)+(-2.2,1.7) node (sou1) [sensor] {Fact}; |
|
259 \path (IR.west)+(-2.2,0.5) node (sou2)[sensor] {Fib}; |
|
260 \path (IR.west)+(-2.2,-0.7) node (sou4)[sensor] {Primes}; |
|
261 \only<2>{\path (IR.west)+(-2.2,-1.9) node (sou3)[sensor] {BrainF**k};} |
|
262 |
|
263 \path [draw,->,line width=1mm] (sou1.east) -- node [above] {} (IR.160); |
|
264 \path [draw,->,line width=1mm] (sou2.east) -- node [above] {} (IR.180); |
|
265 \only<2>{\path [draw,->,line width=1mm] (sou3.east) -- node [above] {} (IR.200);} |
|
266 \path [draw,->,line width=1mm] (sou4.east) -- node [above] {} (IR.190); |
|
267 |
|
268 \path (IR.east)+(2.2, 0.8) node (tar2)[sensor] {JVM}; |
|
269 \path (IR.east)+(2.2,-0.8) node (tar3)[sensor] {LLVM{\small(x86)}}; |
|
270 |
|
271 \path [draw,<-,line width=1mm] (tar2.west) -- node [above] {} (IR.5); |
|
272 \path [draw,<-,line width=1mm] (tar3.west) -- node [above] {} (IR.-5); |
|
273 |
|
274 |
|
275 \end{tikzpicture} |
|
276 \end{frame} |
|
277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
278 |
|
279 |
|
280 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
281 \begin{frame}[c] |
|
282 \frametitle{Dijkstra on Testing} |
|
283 |
|
284 \begin{bubble}[10cm] |
|
285 ``Program testing can be a very effective way to show the |
|
286 presence of bugs, but it is hopelessly inadequate for showing |
|
287 their absence.'' |
|
288 \end{bubble}\bigskip |
|
289 |
|
290 |
|
291 \end{frame} |
|
292 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
293 |
|
294 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
295 \begin{frame}[c] |
|
296 \frametitle{\Large Proving Programs to be Correct} |
|
297 |
|
298 \begin{bubble}[10cm] |
|
299 \small |
|
300 {\bf Theorem:} There are infinitely many prime |
|
301 numbers.\medskip\\ |
|
302 |
|
303 {\bf Proof} \ldots\\ |
|
304 \end{bubble}\bigskip |
|
305 |
|
306 |
|
307 similarly\bigskip |
|
308 |
|
309 \begin{bubble}[10cm] |
|
310 \small |
|
311 {\bf Theorem:} The program is doing what |
|
312 it is supposed to be doing.\medskip |
|
313 |
|
314 {\bf Long, long proof} \ldots\\ |
|
315 \end{bubble}\bigskip\medskip |
|
316 |
|
317 \small This can be a gigantic proof. The only hope is to have |
|
318 help from the computer. `Program' is here to be understood to be |
|
319 quite general (compiler, OS, \ldots). |
|
320 |
|
321 \end{frame} |
|
322 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
323 |
|
324 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
325 |
|
326 \begin{frame}[c] |
|
327 \frametitle{Can This Be Done?} |
|
328 |
|
329 \begin{itemize} |
|
330 \item in 2011, verification of a small C-compiler (CompCert) |
|
331 \begin{itemize} |
|
332 \item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour'' |
|
333 \item is as good as \texttt{gcc -O1}, but much, much less buggy |
|
334 \end{itemize} |
|
335 \end{itemize} |
|
336 |
|
337 \begin{center} |
|
338 \includegraphics[scale=0.12]{../pics/compcert.png} |
|
339 \end{center} |
|
340 |
|
341 \end{frame} |
|
342 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
343 |
|
344 %% ~2,237,800 lines of proof in 474 |
|
345 |
|
346 |
|
347 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
348 \begin{frame}[c] |
|
349 \frametitle{Fuzzy Testing C-Compilers} |
|
350 |
|
351 \begin{itemize} |
|
352 \item tested GCC, LLVM and others by randomly generating |
|
353 C-programs |
|
354 \item found more than 300 bugs in GCC and also |
|
355 many in LLVM (some of them highest-level critical)\bigskip |
|
356 \item about CompCert: |
|
357 |
|
358 \begin{bubble}[10cm]\small ``The striking thing about our CompCert |
|
359 results is that the middle-end bugs we found in all other |
|
360 compilers are absent. As of early 2011, the under-development |
|
361 version of CompCert is the only compiler we have tested for |
|
362 which Csmith cannot find wrong-code errors. This is not for |
|
363 lack of trying: we have devoted about six CPU-years to the |
|
364 task.'' |
|
365 \end{bubble} |
|
366 \end{itemize} |
|
367 |
|
368 \end{frame} |
|
369 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
370 |
|
371 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
372 \begin{frame}[c] |
|
373 \frametitle{seL4 / Isabelle} |
|
374 |
|
375 \begin{itemize} |
|
376 \item verified a microkernel operating system ($\approx$8000 lines of C code)\bigskip |
|
377 \item US DoD has competitions to hack into drones; they found that the |
|
378 isolation guarantees of seL4 hold up\bigskip |
|
379 \item CompCert and seL4 sell their code |
|
380 \end{itemize} |
|
381 |
|
382 \only<2>{ |
|
383 \begin{textblock}{5}(5.5,1.9) |
|
384 \includegraphics[scale=0.25]{../pics/drone.jpg} |
|
385 \end{textblock}} |
|
386 |
|
387 \end{frame} |
|
388 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
389 |
451 |
390 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
452 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
391 |
453 |
392 \begin{frame}[c] |
454 \begin{frame}[c] |
393 \frametitle{Where to go on from here?} |
455 \frametitle{Where to go on from here?} |
394 |
456 |
395 \begin{itemize} |
457 \begin{itemize} |
396 \item Martin Odersky (EPFL)\ldots he is currently throwing out everything |
458 \item Martin Odersky (EPFL) developed Scala 3.0\medskip |
397 and starts again with the dotty compiler for Scala 3.0\medskip |
|
398 |
459 |
399 \item Elm (\url{http://elm-lang.org})\ldots web applications with style\medskip |
460 \item Elm (\url{http://elm-lang.org})\ldots web applications with style\medskip |
400 |
461 |
401 \item Haskell, Ocaml, Standard ML, Scheme, \ldots |
462 \item Haskell, Ocaml, Standard ML, Scheme, \ldots |
402 \end{itemize} |
463 \end{itemize} |