About

The summer school will give a broad overview of software verification techniques, addressing both bottom-up and top-down approaches with a strong focus on the formal representation and reasoning themes. 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; process algebras 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.

The summer school is a satellite event of VSSTE’10 and will be held the two days before the main event: Saturday 14th and Sunday 15th August 2010. It will held at the Edinburgh campus of Heriot-Watt University.

Some pictures from the summer school are available from this link.

Presenters

The following will present at the summer school:

1. •Robert Atkey (University of Strathclyde) & Ewen Maclean (Heriot-Watt University)
   

2. •Alan Bundy & Lucas Dixon (University of Edinburgh)
   

3. •Jane Hillston (University of Edinburgh)
   

4. •Cliff Jones (University of Newcastle)
   

5. •Gerwin Klein (National ICT Australia)
   

6. •J Strother Moore (University of Texas at Austin)
   

7. •Natarajan Shankar (SRI)
   

8. •Graham Steel (INRIA)
   

Programme

Some pictures from the summer school are available from this link.

Saturday

1. •09:00: Registration
   

2. •09:30: J Moore - Machines Reasoning about Machines - 39 Years and Counting [slides]
   

3. •11:00: Coffee break
   

4. •11:30: Gerwin Klein - Specification and Refinement in Operating System Verification [slides]
   

5. •13:00: Lunch
   

6. •14:00: Bob Atkey & Ewen Maclean: Amortised Resource Analysis and Functional Correctness with Separation Logic [slides1, slides2]
   

7. •15:30: Coffee break
   

8. •16:00: Alan Bundy & Lucas Dixon - Planning and Patching Proofs [slides,exercises,solutions]
   

9. •17:30: End
   

Sunday

1. •09:30: Natarajan Shankar - Verification using SAT and SMT solvers [slides]
   

2. •11:00: Coffee break
   

3. •11:30: Graham Steel - Formal Analysis of Key Management APIs [slides]
   

4. •13:00: Lunch
   

5. •14:00: Cliff Jones - Tackling concurrency by reasoning explicitly about inference [slides]
   

6. •15:30: Coffee break
   

7. •16:00: Jane Hillston - From Milner to Markov and Back: Stochastic process algebras and their equivalence relations [slides]
   

8. •17:30: End
   

Recommended Background Material

The following background papers are recommended:

1. •Robert Atkey & Ewen Maclean recommend the following paper for their talk:
   

2. •J. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. [pdf]
   

3. •B. Atkey. Amortised Resource Analysis for Separation Logic. [pdf]
   

4. •Alan Bundy & Lucas Dixon recommend the following paper for their talk:
   

5. •A. Bundy. The Automation Of Proof By Mathematical Induction. Chapter in the "Handbook of Automated Reasoning [url]
   

6. •A. Bundy. Planning and Patching Proof. In AISC 2004 [url]
   

7. •Jane Hillston recommends the following paper for their talk:
   

8. •J. Hillston. Process Algebras for Quantitative Analysis. [url]
   

9. •Cliff Jones recommends the following paper for his talk:
   

10. •C. B. Jones. Accommodating Interference in the Formal Design of Concurrent Object-Based Programs. Formal Methods in System Design, 1996 [url]
    

11. •Gerwin Klein recommends the following paper for his talk:
    

12. •D. Cock, G. Klein and T. Sewell. Secure Microkernels, State Monads and Scalable Refinement. In TPHOL’08 [url]
    

13. •T. Nipkow, L. Paulson and M. Wenzel. A Proof Assistant for Higher-Order Logic (The Isabelle/HOL tutorial) [url]
    

14. •J Strother Moore  recommends the following paper for his talk:
    

15. •M. Kaufmann and J. Moore. Some Key Research Problems in Automated Theorem Proving for Hardware and Software Verification. [pdf]
    

16. •Natarajan Shankar recommends the following paper for his talk:
    

17. •N. Shankar. Automated Deduction for Verification [pdf]
    

18. •Graham Steel recommends the following papers for his talk:
    

19. •S. Delaune, S. Kremer and G. Steel.  Formal Analysis of PKCS#11. In CSF'08, pages 331-344. IEEE Computer Society Press, 2008 [pdf]
    

20. •V. Cortier and G. Steel.  A generic security API for symmetric key management on cryptographic devices.  In ESORICS'09, LNCS 5789, pages 605-620. Springer, 2009 [pdf]
    

21. •C. Cachin and N. Chandran. A secure cryptographic token interface. In Proc. Computer Security Foundations Symposium (CSF-22), pages 141-153. IEEE, July 2009 [pdf]
    

Please let us know if you have any difficulties in getting hold of the papers.

Local Information

Venue

The lectures will be held in the McMillan Lecture room (room G.01 on the ground floor) of the Colin Maclaurin Building. Since the summer school is being held during the weekend, access is only possible through the main entrance (north facing) of Earl Mountbatten building. The venue is building 1 of this campus map, while the entrance is through building 3. For those staying in town, Lothian bus 34 stops just outside the entrance:

Details about getting to and around campus are available by following this link. 

Accommodation

The campus is a short taxi ride from the airport. There is a good bus-link using Lothian buses 25 or 34 (34 stops just outside the school venue).

More details about getting to campus available by following this link. Check-in and check-out is handled in the main reception.

Map