The school consists of eight introductory lectures, each concentrating on an unique aspect of one or both of the overall themes. The topics of the lectures include inductive theorem proving; SAT and SMT solving; proof planning and rippling; rely/guarantee conditions; separation logic; operating system verification; BiGraphs and formal analysis of security.



The school is intended for PhD students and researchers working within one or both of these themes, however familiarity with any of the techniques is not a prerequisite. All lectures are meant to be introductory.

Presenters:

* Robert Atkey (Strathclyde) & Ewen Maclean (Heriot-Watt)

* Alan Bundy & Lucas Dixon (Edinburgh)
* Cliff Jones (Newcastle)
* Gerwin Klein (National ICT Australia)
* Robin Milner (Cambridge/ Edinburgh Universities)
 * J Strother Moore (University of Texas/Austin)

* Natarajan Shankar (SRI)
* Graham Steel (INRIA)