IFIP WG 1.9/2.15 Verified Software

Tenth meeting, Montauban, France, October 2-4, 2016

The tenth meeting of IFIP WG 1.9/2.15 Verified Software is hosted in Montauban, France. On the second and third day (October 3-4), we are having a joint meeting with 2.3 at Bertrand Meyer's Château de Villebrumier, near Montauban.

Accommodation

At Abbaye des Capucins Hôtel.

On Sunday, the meeting is hosted at Abbaye des Capucins. On Monday and Tuesday, it is hosted at Château de Villebrumier and there will be a bus for the ride between the hotel and the château (15 minutes).

Travel

The nearest airport is Toulouse, which has excellent international connections. Then there are at least two options to reach Montauban:

• A taxi from Toulouse airport. The ride takes about 40 minutes. Taxis at Toulouse airport will charge you a lot, so it could be a good idea to share a ride with other participants (see the list below).
• A shuttle from Toulouse airport to Toulouse train station (20 minutes ride, 8 euros) and then a train from Toulouse to Montauban (25 minutes ride, less than 15 euros). There is a 18 minutes walk from Montauban train station to Abbaye des Capucins (unless you take a taxi).

There are also trains from Paris to Montauban. The trip takes 5 hours (there are TGVs, although not at TGV speed all the way yet).

Schedule

Sunday 2 (1.9 only, at Abbaye des Capucins)

• 8am - 9am - welcome coffee
• 9am - 10:30am - session
  • Klaus Havelund (joint work with Sean Kauffman and Rajeev Joshi)
    nfer - A Notation and System for Inferring Event Stream Abstractions
  • Andrew Ireland (joint work with Rajiv Murali, Gudmund Grov, and Martin Ross)
    Modelling System and Accident Scenarios: informal and formal
• coffee break
• 11am - 12:30pm - session 2 (2 talks)
  • Gary Leavens (joint work with David Naumann, Hridesh Rajan, Tomoyuki Aotani)
    Specifying and Verifying Advanced Control Structures
  • Marcello Frias
    Stryker: (More) Scalable Specification-Based Bug Fixing
• lunch
• 2pm - 3:30pm - session 3 (2 talks)
  • Naijun Zhan
    Formal Design of Embedded Systems
  • Arie Gurfinkel
    Algorithmic Logic-Based Verification: Parameterized Systems
• coffee break
• 4pm - 5pm - session 4 (2 shorter talks)
  • Gerhard Shellhorn
    A thread-Local Proof Technique for Starvation-Freedom
  • Jean-Christophe Filliâtre
    A Verified OCaml Library (with a focus on iteration)
• 5pm - no later than 6pm - members only

Monday 3 (with 2.3, at Château de Villebrumier)

   9:30am - 6pm

Tuesday 4 (with 2.3, at Château de Villebrumier)

   9:30am - 3pm

Participants

• June Andronick (invited)
• Andrew Butterfield (invited)
• Ernie Cohen
• Jean-Christophe Filliâtre (chair)
• Marcello Frias (invited)
• Philippa Gardner (invited)
• Arie Gurfinkel (invited)
• Klaus Havelund
• Andrew Ireland
• Gary Leavens
• Bart Jacobs
• Cliff Jones
• Andreas Podelski
• Natarajan Shankar (secretary)
• Gerhard Shellhorn (invited)
• Alex Summers (invited)
• Jim Woodcock
• Naijun Zhan (invited)

---

Last updated: July 29, 2016