Monday	Tuesday	Wednesday	Thursday	Friday
Room
CSE/102	ATSE
CSE/082	HOFM	MoKMaSD	SEFM	SEFM	SEFM
CSE/083		VERY*SCART

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