Recommended reading papers posted.
Software Reliability 2016/2017 web site goes live.
CC = Cristian Cadar, AD = Alastair Donaldson, LP = Luís Pina (see Team).
11:00 Lecture: Introduction (CC+AD, 144)
12:00 Lecture: Verification condition generation for loop- and call-free programs, 1 (AD, 144)
11:00 Lecture: Verification condition generation for loop- and call-free programs, 2 (AD, 311)
12:00 Lecture: Procedure and loop summarisation, 1 (AD, 311)
11:00 Lecture: Procedure and loop summarisation, 2 (AD, 144)
12:00 Lecture: Bounded model checking (AD, 144)
12:00: Deadline for coursework group formation on CATe
11:00 Lecture: Dynamic symbolic execution, 1 (CC, 311)
12:00 Lecture: Dynamic symbolic execution, 2 (CC, 311)
11:00 No class
12:00 No class
11:00 Tutorial (LP, 311)
12:00 No class
18:00: Deadline: part 1 of coursework
11:00 Lecture: SAT solving: basics and DPLL, 1 (CC, 144)
12:00 Lecture: SAT solving: basics and DPLL, 2 (CC, 144)
11:00 Lecture: SAT and SMT constraint solving (CC, 311)
12:00 Tutorial (LP, 311)
11:00 Lecture: Invariant generation using Houdini, 1 (AD, 144)
12:00 Lecture: Invariant generation using Houdini, 2 (AD, 144)
11:00 Lecture: The lockset algorithm and Eraser (CC, 311)
12:00 Lecture: Systematic testing for concurrent programs (AD, 311)
11:00 Tutorial on advanced coursework issues (AD, 144)
12:00 No class
11:00 Demo: the KLEE symbolic execution tool (CC, 311)
12:00 Tutorial (LP, 311)
11:00 Lecture: Undefined behaviour (AD, 144)
12:00 Lecture: Detecting compiler bugs and unstable code (CC, 144)
11:00 Guest lecture from Rod Chapman, Altran (311)
12:00 Demo from Rod Chapman, followed by material on compiler testing (CC, 311)
18:00: Deadline: part 2 of coursework
11:00 Tutorial (LP, 144)
12:00 Lecture: Safe C compilers (CC, 144)
11:00 Lecture: Program analysis for security (CC, 311)
12:00 Combined tutorial on recent topics and lecture on program analysis for security (LP/CC, 311)
We are happy to run a revision lecture, or possibly two, during this week, if there is a demand for this. Time and place to be determined.