9 abbreviation |
9 abbreviation |
10 "update2 p a \<equiv> update a p" |
10 "update2 p a \<equiv> update a p" |
11 |
11 |
12 |
12 |
13 notation (latex output) |
13 notation (latex output) |
14 Cons ("_::_" [48,47] 48) and |
14 Cons ("_::_" [48,47] 68) and |
|
15 append ("_@_" [65, 64] 65) and |
15 Oc ("1") and |
16 Oc ("1") and |
16 Bk ("0") and |
17 Bk ("0") and |
17 exponent ("_\<^bsup>_\<^esup>") and |
18 exponent ("_\<^bsup>_\<^esup>" [107] 109) and |
18 inv_begin0 ("I\<^isub>0") and |
19 inv_begin0 ("I\<^isub>0") and |
19 inv_begin1 ("I\<^isub>1") and |
20 inv_begin1 ("I\<^isub>1") and |
20 inv_begin2 ("I\<^isub>2") and |
21 inv_begin2 ("I\<^isub>2") and |
21 inv_begin3 ("I\<^isub>3") and |
22 inv_begin3 ("I\<^isub>3") and |
22 inv_begin4 ("I\<^isub>4") and |
23 inv_begin4 ("I\<^isub>4") and |
84 \mode<presentation>{ |
85 \mode<presentation>{ |
85 \begin{frame} |
86 \begin{frame} |
86 \frametitle{% |
87 \frametitle{% |
87 \begin{tabular}{@ {}c@ {}} |
88 \begin{tabular}{@ {}c@ {}} |
88 \\[-3mm] |
89 \\[-3mm] |
89 \Large Reasoning about Turing Machines\\[-1mm] |
90 {\fontsize{20}{20}\selectfont{}Mechanising Turing Machines and}\\[-2mm] |
90 \Large and Low-Level Code\\[-3mm] |
91 {\fontsize{20}{20}\selectfont{}Computability Theory in Isabelle}\\[-3mm] |
91 \end{tabular}} |
92 \end{tabular}} |
92 |
93 |
93 \begin{center} |
94 \bigskip\medskip\medskip |
94 Christian Urban\\[1mm] |
|
95 %%\small King's College London |
|
96 \end{center}\bigskip |
|
97 |
95 |
98 \begin{center} |
96 \begin{center} |
99 in cooperation with Jian Xu and Xingyuan Zhang |
97 \begin{tabular}{c@ {\hspace{1cm}}c} |
100 \end{center} |
98 \includegraphics[scale=0.29]{jian.jpg} & |
101 \end{frame}} |
99 \includegraphics[scale=0.034]{xingyuan.jpg} \\ |
102 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
100 Jian Xu & Xingyuan Zhang\\[-3mm] |
103 *} |
101 \end{tabular}\\[3mm] |
104 |
102 \small PLA University of Science and Technology |
105 text_raw {* |
103 \end{center} |
106 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
104 |
107 \mode<presentation>{ |
105 \begin{center} |
108 \begin{frame}[c] |
106 Christian Urban\\[0mm] |
109 \frametitle{A Trend in Verification}% |
107 \small King's College London |
110 |
108 \end{center} |
111 \begin{itemize} |
109 \end{frame}} |
112 \item in the past:\\ |
110 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
113 \begin{quote} |
111 *} |
114 model a problem mathematically and proof properties about the |
112 |
115 model |
113 |
116 \end{quote}\bigskip |
114 text_raw {* |
117 |
115 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
118 \item needs elegance, is still very hard\bigskip\pause |
116 \mode<presentation>{ |
119 |
117 \begin{frame}[c] |
120 \item does not help with ensuring the correctness of running programs |
118 \frametitle{Why Turing Machines?}% |
121 \end{itemize} |
119 |
122 |
120 \begin{itemize} |
123 \end{frame}} |
121 \item At the beginning, it was just a student project |
124 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
122 about computability.\smallskip |
125 *} |
123 |
126 |
124 \begin{center} |
127 text_raw {* |
125 \begin{tabular}{c} |
128 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
126 \includegraphics[scale=0.3]{boolos.jpg}\\[-2mm] |
129 \mode<presentation>{ |
127 \footnotesize Computability and Logic (5th.~ed)\\[-2mm] |
130 \begin{frame}[c] |
128 \footnotesize Boolos, Burgess and Jeffrey\\[2mm] |
131 \frametitle{A Trend in Verification}% |
129 \end{tabular} |
132 |
|
133 \begin{itemize} |
|
134 \item make the specification executable (e.g.~Compcert)\bigskip\pause |
|
135 |
|
136 you would expect the trend would be to for example model C, implement |
|
137 your programs in C and verify the programs written in C (e.g.~seL4) |
|
138 \end{itemize} |
|
139 |
|
140 \end{frame}} |
|
141 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
142 *} |
|
143 |
|
144 text_raw {* |
|
145 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
146 \mode<presentation>{ |
|
147 \begin{frame}[c] |
|
148 \frametitle{A Trend in Verification}% |
|
149 |
|
150 \begin{itemize} |
|
151 \item but actually people start to verify machine code directly |
|
152 (e.g.~bignum arithmetic implemented in x86-64 -- 700 instructions) |
|
153 |
|
154 \item CPU models exists, but the strategy is to use a small subset |
|
155 which you use in your programs |
|
156 \end{itemize} |
|
157 |
|
158 \end{frame}} |
|
159 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
160 *} |
|
161 |
|
162 text_raw {* |
|
163 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
164 \mode<presentation>{ |
|
165 \begin{frame}[c] |
|
166 \frametitle{Why Turing Machines}% |
|
167 |
|
168 \begin{itemize} |
|
169 \item at the beginning it was just a nice student project |
|
170 about computability |
|
171 |
|
172 \begin{center} |
|
173 \includegraphics[scale=0.3]{boolos.jpg} |
|
174 \end{center} |
130 \end{center} |
175 |
131 |
176 \item found an inconsistency in the definition of halting computations |
132 \item found an inconsistency in the definition of halting computations |
177 (Chap.~3 vs Chap.~8) |
133 (Chap.~3 vs Chap.~8) |
178 \pause |
134 \end{itemize} |
179 |
135 |
180 \item \small Norrish formalised computability via lambda-calculus (and nominal); |
136 \end{frame}} |
181 Asperti and Riccioti formalised TMs but didn't get proper UTM |
137 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
182 \end{itemize} |
138 *} |
183 |
139 |
|
140 text_raw {* |
|
141 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
142 \mode<presentation>{ |
|
143 \begin{frame}[c] |
|
144 \frametitle{Some Previous Work}% |
|
145 |
|
146 \begin{itemize} |
|
147 \item Norrish formalised computability theory in HOL starting |
|
148 from the lambda-calculus |
|
149 \begin{itemize} |
|
150 \item \textcolor{gray}{for technical reasons we could not follow him} |
|
151 \item \textcolor{gray}{some proofs use TMs (Wang tilings)} |
|
152 \end{itemize} |
|
153 |
|
154 |
|
155 |
|
156 \bigskip |
|
157 |
|
158 \item Asperti and Ricciotti formalised TMs in Matita |
|
159 \end{itemize} |
184 |
160 |
185 \end{frame}} |
161 \end{frame}} |
186 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
162 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
187 *} |
163 *} |
188 |
164 |
220 \node [anchor=base] at (-2.2,0.2) {\ldots}; |
196 \node [anchor=base] at (-2.2,0.2) {\ldots}; |
221 \node [anchor=base] at ( 2.3,0.2) {\ldots}; |
197 \node [anchor=base] at ( 2.3,0.2) {\ldots}; |
222 \end{tikzpicture} |
198 \end{tikzpicture} |
223 \end{center} |
199 \end{center} |
224 |
200 |
225 \item steps function |
201 \item @{text steps} function: |
226 |
202 |
227 \begin{quote} |
203 \begin{quote}\rm |
228 What does the tape look like after the TM has executed n steps? |
204 What does the TM claclulate after it has executed @{text n} steps? |
229 \end{quote}\pause |
205 \end{quote}\pause |
230 |
206 |
231 designate the 0-state as halting state and remain there forever |
207 \item designate the @{text 0}-state as \"halting state\" and remain there |
|
208 forever, i.e.~have a @{text Nop}-action |
|
209 \end{itemize} |
|
210 |
|
211 \end{frame}} |
|
212 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
213 *} |
|
214 |
|
215 text_raw {* |
|
216 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
217 \mode<presentation>{ |
|
218 \begin{frame}[c] |
|
219 \frametitle{Register Machines}% |
|
220 |
|
221 \begin{itemize} |
|
222 \item instructions |
|
223 |
|
224 \begin{center} |
|
225 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
|
226 @{text "I"} & $::=$ & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\ |
|
227 & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & if content of @{text R} is non-zero,\\ |
|
228 & & & then decrement it by one\\ |
|
229 & & & otherwise jump to instruction @{text L}\\ |
|
230 & $\mid$ & @{term "Goto L\<iota>"} & jump to instruction @{text L} |
|
231 \end{tabular} |
|
232 \end{center} |
|
233 |
232 \end{itemize} |
234 \end{itemize} |
233 |
235 |
234 \end{frame}} |
236 \end{frame}} |
235 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
237 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
236 *} |
238 *} |
248 \begin{center} |
250 \begin{center} |
249 \begin{tikzpicture}[scale=0.7] |
251 \begin{tikzpicture}[scale=0.7] |
250 \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$}; |
252 \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$}; |
251 \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$}; |
253 \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$}; |
252 \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$}; |
254 \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$}; |
253 \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{\text{cbegin}}^{}$}; |
255 \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{@{text cbegin}}^{}$}; |
254 \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{\text{cloop}}^{}$}; |
256 \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{@{text cloop}}^{}$}; |
255 \node [anchor=base] at (10.5,-0.8) {\small$\overbrace{\text{cend}}^{}$}; |
257 \node [anchor=base] at (10.5,-0.8) {\small$\overbrace{@{text cend}}^{}$}; |
256 |
258 |
257 |
259 |
258 \begin{scope}[shift={(0.5,0)}] |
260 \begin{scope}[shift={(0.5,0)}] |
259 \draw[very thick] (-0.25,0) -- ( 1.25,0); |
261 \draw[very thick] (-0.25,0) -- ( 1.25,0); |
260 \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5); |
262 \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5); |
403 \mode<presentation>{ |
405 \mode<presentation>{ |
404 \begin{frame}[c] |
406 \begin{frame}[c] |
405 \frametitle{Hoare Reasoning}% |
407 \frametitle{Hoare Reasoning}% |
406 |
408 |
407 \begin{itemize} |
409 \begin{itemize} |
408 \item reasoning is still quite difficult---invariants |
410 \item reasoning is still quite demanding;\\ |
|
411 the invariants of the copy-machine:\\[-5mm]\mbox{} |
409 |
412 |
410 \footnotesize |
413 \footnotesize |
411 \begin{center} |
414 \begin{center} |
412 \begin{tabular}{@ {\hspace{-4mm}}lcl@ {\hspace{-0.9cm}}l@ {}} |
415 \begin{tabular}{@ {\hspace{-5mm}}c@ {}} |
|
416 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {\hspace{-0.9cm}}l@ {}} |
413 \hline |
417 \hline |
414 @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\ |
418 @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\ |
415 @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\ |
419 @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\ |
416 @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\ |
420 @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\ |
417 @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\ |
421 @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\ |
424 \hline |
428 \hline |
425 @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\ |
429 @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\ |
426 @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\ |
430 @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\ |
427 \hline |
431 \hline |
428 \end{tabular} |
432 \end{tabular} |
429 \end{center} |
433 \end{tabular} |
430 |
434 \end{center} |
431 \end{itemize} |
435 |
432 |
436 \end{itemize} |
433 \end{frame}} |
437 |
434 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
438 \end{frame}} |
435 *} |
439 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
436 |
440 *} |
437 text_raw {* |
441 |
438 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
442 |
439 \mode<presentation>{ |
|
440 \begin{frame}[c] |
|
441 \frametitle{Register Machines}% |
|
442 |
|
443 \begin{itemize} |
|
444 \item instructions |
|
445 |
|
446 \begin{center} |
|
447 \begin{tabular}{rcl@ {\hspace{10mm}}l} |
|
448 @{text "I"} & $::=$ & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\ |
|
449 & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & if content of @{text R} is non-zero,\\ |
|
450 & & & then decrement it by one\\ |
|
451 & & & otherwise jump to instruction @{text L}\\ |
|
452 & $\mid$ & @{term "Goto L\<iota>"} & jump to instruction @{text L} |
|
453 \end{tabular} |
|
454 \end{center} |
|
455 |
|
456 \end{itemize} |
|
457 |
|
458 \end{frame}} |
|
459 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
460 *} |
|
461 |
443 |
462 text_raw {* |
444 text_raw {* |
463 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
445 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
464 \mode<presentation>{ |
446 \mode<presentation>{ |
465 \begin{frame}[c] |
447 \begin{frame}[c] |