Software Reliability 2016/2017
MEng 4 and MSc selected specialisms, Department of Computing
Imperial College London
©

NEWS

17 October 2016

Recommended reading papers posted.

06 October 2016

Software Reliability 2016/2017 web site goes live.

Timetable

The timetable is provisional. It is subject to change before the course starts, and we will likely deviate from it a bit during the course depending how long the material takes to deliver in practice, and according to how much discussion there is during the lectures (in previous years there has been a lot, which was great!)

CC = Cristian Cadar, AD = Alastair Donaldson, LP = Luís Pina (see Team).

Week 2

Tuesday 11 October

11:00 Lecture: Introduction (CC+AD, 144)

12:00 Lecture: Verification condition generation for loop- and call-free programs, 1 (AD, 144)

Friday 14 October

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)

Week 3

Tuesday 18 October

11:00 Lecture: Procedure and loop summarisation, 2 (AD, 144)

12:00 Lecture: Bounded model checking (AD, 144)

Wednesday 19 October

12:00: Deadline for coursework group formation on CATe

Friday 21 October

11:00 Lecture: Dynamic symbolic execution, 1 (CC, 311)

12:00 Lecture: Dynamic symbolic execution, 2 (CC, 311)

Week 4

Tuesday 25 October

11:00 No class

12:00 No class

Friday 28 October

11:00 Tutorial (LP, 311)

12:00 No class

18:00: Deadline: part 1 of coursework

Week 5

Tuesday 1 November

11:00 Lecture: SAT solving: basics and DPLL, 1 (CC, 144)

12:00 Lecture: SAT solving: basics and DPLL, 2 (CC, 144)

Friday 4 November

11:00 Lecture: SAT and SMT constraint solving (CC, 311)

12:00 Tutorial (LP, 311)

Week 6

Tuesday 8 November

11:00 Lecture: Invariant generation using Houdini, 1 (AD, 144)

12:00 Lecture: Invariant generation using Houdini, 2 (AD, 144)

Friday 11 November

11:00 Lecture: The lockset algorithm and Eraser (CC, 311)

12:00 Lecture: Systematic testing for concurrent programs (AD, 311)

Week 7

Tuesday 15 November

11:00 Tutorial on advanced coursework issues (AD, 144)

12:00 No class

Friday 18 November

11:00 Demo: the KLEE symbolic execution tool (CC, 311)

12:00 Tutorial (LP, 311)

Week 8

Tuesday 22 November

11:00 Lecture: Undefined behaviour (AD, 144)

12:00 Lecture: Detecting compiler bugs and unstable code (CC, 144)

Friday 25 November

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

Week 9

Tuesday 29 November

11:00 Tutorial (LP, 144)

12:00 Lecture: Safe C compilers (CC, 144)

Friday 2 December

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)

Week 10

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.