Monday Tuesday Wednesday Thursday Friday

Monday, 7 September
09:00 - 18:00 Workshop 1: ATSE
6th Workshop on Automating Test case design, Selection and Evaluation
09:00 - 18:00 Workshop 2: HOFM
Human-Oriented Formal Methods: From Readability to Automation
Tuesday, 8 September
09:00 - 18:00 Workshop 3: MoKMaSD
4th International Symposium on Modelling and Knowledge Management applications: Systems and Domains
09:00 - 18:00 Workshop 4: VERY*SCART
The Art of Service Composition and Formal Verification for Self-* Systems (joint workshop comprising VERY* and SCART)
Wednesday, 9 September
08:30 - 09:15 Main Conference Registration
09:15 - 09:30 Opening
09:30 - 10:30 Keynote
Session chair: Jim Woodcock
Invited speaker: Peter O’Hearn
(Engineering Manager at Facebook & Professor of Computer Science at University College London)
Moving Fast with Software Verification
10:30 - 11:00 Coffee break
11:00 - 12:30 Session 1 - Program Verification I
Session chair: Ian Hayes
  • Jan Tobias Mühlberg, David White, Mike Dodds, Gerald Luettgen and Frank Piessens - Learning Assertions to Verify Linked-List Programs
  • Gijs Vanspauwen and Bart Jacobs - Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications
  • Afshin Amighi, Saeed Darabi, Stefan Blom and Marieke Huisman - Specification and Verification of Atomic Operations in GPGPU Programs
12:30 - 14:00 Lunch
14:00 - 15:25 Session 2 - Testing
Session chair: Rida Bazzi
  • Stefan Huster, Sebastian Burg, Hanno Eichelberger, Jo Laufenberg, Jürgen Ruf, Thomas Kropf and Wolfgang Rosenstiel - Efficient Testing of Different Loop Paths
  • Aymerick Savary, Marc Frappier, Michael Leuschel and Jean-Louis Lanet - Model-Based Robustness Testing in Event-B using Mutation
  • Simone Hanazumi and Ana C. V. de Melo - On the Testability of Properties Patterns (short paper)
15:25 - 16:00 Coffee break
16:00 - 17:25 Session 3 - Certification
Session chair: Antonio Cerone
  • Marie-Christine Jakobs - Speed Up Configurable Certificate Validation by Certificate Reduction and Partitionings
  • Mojgan Kamali, Peter Höfner, Maryam Kamali and Luigia Petre - Formal Analysis of Proactive, Distributed Routing
  • Kim Völlinger and Wolfgang Reisig - Certification of Distributed Algorithms Solving Problems with Optimal Substructure (short paper)
18:00 - 20:00 Welcome Reception sponsored by IBM
Thursday, 10 September
09:30 - 10:30 Keynote
Session chair: Radu Calinescu
Invited speaker: Cliff Jones
(Professor of Computing Science at Newcastle University)
Reasoning about Separation using Abstraction and Reification
10:30 - 11:00 Coffee break
11:00 - 12:30 Session 4 - Formal Specification and Proof
Session chair: Stefania Gnesi
  • Sebastian Krings, Jens Bendisposto and Michael Leuschel - From Failure to Proof: The ProB Disprover for B and Event-B
  • Adriaan Larmuseau and Dave Clarke - Formalizing a Secure Foreign Function Interface
  • Jun Shen and Rida A. Bazzi - A Formal Study of Backward Compatible Dynamic Software Updates
12:30 - 14:00 Lunch
14:00 - 15:25 Session 5 - Testing and Model Checking
Session chair: Gerald Luettgen
  • Herbert Rocha, Raimundo Barreto and Lucas Cordeiro - Memory Management Test-Case Generation of C Programs using Bounded Model Checking
  • Petr Ročkai, Vladimír Štill and Jiří Barnat - Techniques for Memory-Efficient Model Checking of C and C++ Code
  • Gustavo Carvalho, Flavia Barros, Ana Carvalho, Ana Cavalcanti, Alexandre Mota and Augusto Sampaio - NAT2TEST Tool: from Natural Language Requirements to Test Cases based on CSP (short tool paper)
15:25 - 16:00 Coffee break
16:00 - 17:00 Session 6 - Planning
Session chair: Francesco Tiezzi
  • Roykrong Sukkerd, David Garlan and Reid Simmons - Task Planning of Cyber-Human Systems
  • Michał Knapik, Artur Niewiadomski and Wojciech Penczek - Generating None-Plans in Order to Find Plans
19:30 - 23:00 Conference banquet
Friday, 11 September
09:30 - 10:30 Keynote
Session chair: Bernhard Rumpe
Invited speaker: Edward A. Lee
(Professor of Electrical Engineering & Computer Sciences at University of California at Berkeley)
The Internet of Important Things
10:30 - 11:00 Coffee break
11:00 - 12:25 Session 7 - Modelling and Model Transformation
Session chair: Ana C. V. de Melo
  • Rocco De Nicola, Alessandro Maggi, Marinella Petrocchi, Angelo Spognardi and Francesco Tiezzi - Twitlang(er): interactions modeling language (and interpreter) for Twitter
  • Maurice H. ter Beek, Ferruccio Damiani, Stefania Gnesi, Franco Mazzanti and Luca Paolini - From Featured Transition Systems to Modal Transition Systems with Variability Constraints
  • Zamira Daw and Rance Cleaveland - An extensible operational semantics for UML activity diagrams (short paper)
12:25 - 14:00 Lunch
14:00 - 15:20 Session 8 - Program Verification II
Session chair: Michael Leuschel
  • Stefan Blom, Marieke Huisman and Marina Zaharieva-Stojanovski - History-based Verification of Functional Behaviour of Concurrent Programs
  • Christian Colombo, Gabriel Dimech and Adrian Francalanza - Investigating Instrumentation Techniques for ESB Runtime Verification (short paper)
  • Robert Clarisó, Carlos A. González and Jordi Cabot - Towards Domain Refinement for UML/OCL Bounded Verification (short paper)
15:20 - 15:40 Closing session
15:40 - 16:10 Coffee break and participant departure

Leave a Reply