|
|
| Topic |
Slides |
| Introduction |
1 - 5 |
| Hoare’s notation |
7 - 11 |
| Formal proofs |
12 - 16 |
| Partial and total correctness |
17 - 19 |
| Example specification |
20 - 25 |
| Review of predicate calculus |
26 - 34 |
| Floyd-Hoare Logic |
35 - 59 |
| How does one find an invariant |
60 - 62 |
| Additional and derived rules |
63 - 72 |
| Forwards and backwards proof |
73 - 79 |
| Annotations |
80 - 82, 92 - 93 |
| Mechanizing verification |
83 - 86 |
| Verification conditions |
87 - 112 |
| Weakest preconditions |
113 121 |
| Strongest postconditions |
122 - 133 |
| Total correctness |
134 - 154 |
| Soundness and completeness |
155 - 179 |
| Overview of additional topics |
180 - 181 |
| Arrays |
182 - 190 |
| Blocks and local variables |
191 - 194 |
FOR-commands |
196 - 213 |
| Axiomatic semantics and Clarke’s theorem |
214 - 215 |
| Refinement |
216 - 251 |
| Separation logic |
252 - 293 |
| Conclusion |
294 |