Fmics2013

Programme

Day 1 -- Monday 23 September

09:45 - 10:00 Welcome

10:00 – 11:00 Keynote 1 (jointly with FM-RAIL-BOK)

Twenty-Five Years of Formal Methods and Railways: What Next? -- Alessandro Fantechi, Università di Firenze

11:00 - 11:30 Coffee Break

11:30 – 13:00 Session 1 -- Safety and Reliability

  • HyRev: A tool for the automatic generation of real-time routines for enabling fail-safe control in a class of safety-critical embedded systems using backwards reachability analysis -- Hallstein Asheim Hansen (slides)
  • Formal Reliability Analysis of Protective Relays in Power Distribution Systems -- Adil Khurram, Haider Ali, Arham Tariq and Osman Hasan (slides)
  • Formal Methods for the Analysis of Critical Control Systems Models: Combining Non-Linear and Linear Analyses -- Adrien Champion, Rémi Delmas, Michael Dierkes, Pierre-Loic Garoche, Romain Jobredeaux and Pierre Roux

13:00 - 14:30 Lunch

14:30 – 16:00 Session 2 -- Programmable Devices

  • Complex Digital System Design: a methodology and its application to medical implants -- Helene Leroux, Karen Godary-Dejean and David Andreu (slides)
  • On the Effectiveness of Assertion-Based Verification in an Industrial Context -- Laurence Pierre, Fabrice Pancher, Rodolphe Suescun and Jérôme Quévremont (slides)
  • Predicate Abstraction for Programmable Logic Controllers -- Sebastian Biallas, Mirco Giacobbe and Stefan Kowalewski (slides)

16:00 - 16:30 Coffee Break

16:30 – 18:00 Session 3 -- Consistency

  • Boolean Quantifier Elimination for Automotive Configuration - A Case Study -- Christoph Zengler and Wolfgang Küchlin (slides)
  • Auditing User-Provided Axioms in Software Verification Conditions -- Paul Jackson, Florian Schanda and Angela Wallenburg (slides)

21:00 Dinner

Day 2 -- Tuesday 24 September

09:45 - 10:00 Welcome

10:00 – 11:00 Keynote 2

TrustInSoft: Industrial Formal Methods to Protect Security-Sensitive Systems -- Benjamin Monate, TrustInSoft

11:00 - 11:30 Coffee Break

11:30 – 13:00 Session 4 -- Feedback from Industrial Applications

  • Study on the Barriers to the Industrial Adoption of Formal Methods -- Jennifer Davis, Matthew Clark, Darren Cofer, Aaron Fifarek, Jacob Hinchman, Jonathan Hoffman, Brian Hulbert, Steven Miller and Lucas Wagner (slides)
  • Manager Guidelines for the Industrial Deployment of Formal Methods -- Christophe Ponsard, Jean-Christophe Deprez and Renaud De Landtsheer (slides)
  • An outline workflow for practical formal verification from software requirements to object code -- Darren Sexton (slides)

13:00 - 14:30 Lunch

14:30 – 15:30 Session 5 -- Protocol Analysis

  • Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip -- Abderahman Kriouile and Wendelin Serwe (slides)
  • Specification and Verification using Alloy of Optimistic Access Control for Distributed Collaborative Editors -- Aurel Randolph, Abdessamad Imine, Hanifa Boucheneb and Alejandro Quintero

15:30 - 16:00 Closing

16:00 - 16:30 Coffee Break

16:30 – 18:00 FMICS management meeting (members only)