Programme

Note. The two day SICSA Summer School on Formal Reasoning & Representation of Complex Systems will be held on August 14th and 15th 2010. The programme details for the summer school can be found here.

Monday 16th August

1. •08:00-09:00: Registration (coffee & pastry from 8:20)
   

2. •09:00-09:30: Conference opening
   

3. •09.30-10.30: Keynote 1 (chair: Gary T. Leavens): Thomas Ball, Brian Hackett, Shuvendu Lahiri, Shaz Qadeer and Julien Vanegue. Towards Scalable Modular Checking Of User-Defined Properties (presented by Tom Ball)
   

1. •10.30-11.00: Coffee & Tea
   

1. •Regular Papers Session 1 (chair: Joe Kiniry)
   

2. •11.00-11.30: Ali Sezgin, Serdar Tasiran and Shaz Qadeer. Tressa: Claiming the Future
   

3. •11.30-12.00: Eyad Alkassar, Mark Hillebrand, Wolfgang Paul and Elena Petrova. Automated Verification of a Small Hypervisor
   

4. •12.00-12.30: Tom Ridge. A Rely-Guarantee proof system for x86-TSO
   

1. •12.30-14.00: Lunch
   

1. •14.00-15.00: Poster Session (Coffee & Tea will be served during this session)
   

1. •15.00-17.00: Invited Tools Presentations and Demos  (chair: Graham Steel)
   

2. •Colin O’Halloran - ClawZ/Circus
   

3. •Bart Jacobs - VeriFast
   

4. •Michael Jastram - The ProB Animator and Model Checker
   

5. •Joe Kiniry -- Tool-supported Refinement-centric Analysis, Design, Development and Verification
   

1. •18.00-19.00: Welcome Reception
   

2. •19.00-21.00: Buffet Dinner
   

Tuesday 17th August

1. •09.30-10.30: Keynote 2 (chair: Peter O’Hearn): Gerwin Klein. The L4.verified Project - Next Steps
   

1. •10.30-11.00: Coffee & Tea
   

1. •Regular Papers Session 2 (chair: Matthew Parkinson)
   

2. •11.00-11.30: Eyad Alkassar, Wolfgang Paul, Artem Starostin and Alexandra Tsyban. Pervasive Verification of an OS Microkernel: Inline Assembly, Memory Consumption, Concurrent Devices
   

3. •11.30-12.00: Michael Jastram, Stefan Hallerstede, Michael Leuschel and Aryldo G Russo Jr. An Approach of Requirements Tracing in Formal Refinement
   

4. •12.00-12.30: Rosemary Monahan and Rustan Leino. Dafny meets the Verification Benchmarks Challenge
   

1. •12.30-14.00: Lunch
   

1. •14.00-15.00: Discussion Panel: Challenges & Collaborative Opportunities
   

2. •Cliff Jones (chair)
   

3. •Philippa Gardner
   

4. •J Moore
   

5. •Peter Mueller
   

6. •Matthew Parkinson
   

1. •15.00-15.30: Coffee & Tea
   

1. •Regular Papers Session 3 (chair: Tiziana Margaria)
   

2. •15.30-16.00: Nadia Polikarpova, Carlo A. Furia and Bertrand Meyer. Specifying Reusable Components
   

3. •16.00-16.30: Magnus O. Myreen. Reusable verification of a copying collector
   

4. •16.30-17.00: Michael Barnett and Rustan Leino. To Goto Where No Statement Has Gone Before
   

1. •18.00: Transportation to City Centre
   

2. •19.00: SICSA Sponsored Drinks Reception (Informatics Forum, University of Edinburgh)
   

Wednesday 18th August

1. •09.00-10.00: Keynote 3 (chair: Phillipa Gardner): Matthew Parkinson. The Next 700 Separation Logics
   

1. •10.00-10.30: Coffee & Tea
   

1. •Regular Papers Session 4 (chair: Leo Freitas)
   

2. •10.30-11.00: Stan Rosenberg, Anindya Banerjee and David Naumann. Local Reasoning and Dynamic Framing for the Composite Pattern and its Clients
   

3. •11.00-11.30: Thomas Dinsdale-Young, Philippa Gardner and Mark Wheelhouse. Locality Refinement
   

1. •11.30-12.00: Verification Competition Presentation (Organisers: Natarajan Shankar & Peter Mueller)
   

1. •12.00-13.00: Lunch
   

1. •13.00-14.00: THEORY Workshop (chairs: David Naumann, Hongseok Yang & Peter Mueller)
   

2. •Philippa Gardner, Gareth Smitth and Adam Wright. Local Reasoning about Mashups
   

3. •Christopher M. Poskitt and Detlef Plump. Hoare Logic for Graph Programs
   

1. •14.00-14.30: Coffee & Tea
   

1. •14.30-16.00: THEORY Workshop (chairs: David Naumann, Hongseok Yang & Peter Mueller)
   

2. •Thomas Tuerk. Local Reasoning about While-Loops
   

3. •Chenguang Luo, Guanhua He, Shengchao Qin and Wei-Ngan Chin. Loop Invariant Synthesis in a Combined Domain (Extended Abstract)
   

4. •Lenart Beringer. Relational program logics and self-composition
   

1. •16.00-18.00: Verification Competition - solution has to be submitted by 18:00 (Organisers: Natarajan Shankar & Peter Mueller)
   

1. •19.00-23.00: Conference Banquet
   

Thursday 19th August

1. •09.30-10.30: TOOLS & EXPERIMENTS Workshop (chairs: Tiziana Margaria, Rajeev Joshi  & Peter Mueller)
   

2. •Bart Jacobs, Jan Smans and Frank Piessens. VeriFast: Imperative Programs as Proofs
   

3. •Zoe Andrews, Annabelle McIver, Larissa Meinicke and Carroll Morgan. Probabilistic Aspects of Flash Filestores
   

4. •Ewen Maclean, Andrew Ireland and Gudmund Grov. Functional Correctness for Pointer Programs
   

1. •10.30-11.00: Coffee & Tea
   

1. •11.00-12.30: TOOLS & EXPERIMENTS Workshop (chairs: Tiziana Margaria, Rajeev Joshi  & Peter Mueller)
   

2. •Gudmund Grov and Cliff Jones. AI4FM - A new project seeking challenges!
   

3. •Derek Bronish and Bruce Weide. A Review of Verification Benchmark Solutions Using Dafny
   

4. •Rustan Leino and Michael Moskal. VACID-0: Verification of Ample Correctness of Invariants of Data-structures, Edition 0
   

1. •Verification Competition Result Announcement (Organisers: Natarajan Shankar & Peter Mueller)
   

1. •12.30-13.00: Plenary session & conference close (chair: Andrew Ireland)
   

1. •13.00-14.00: Lunch