Program

Day 1: April 17, 2018 (Tuesday)	8:15 - 5:30
Day 2: April 18, 2018 (Wednesday)	8:30 - 5:30
Day 3: April 19, 2018 (Thursday)	8:30 - 11:45

Times of Talks

• Keynote Speakers: 1h.
• Regular Papers: 30min.
• Short Papers: 15min.

DAY 1: April 17, 2018 (Tuesday)

   7:30 - 8:15 Registration

   8:15 - 8:30 Opening

• Anthony Narkawicz (NASA)

   8:30 - 9:30 Invited Talk (Chair: Aaron Dutle)

• Ricky Butler (NASA). 30 Years of Formal Methods at NASA Langley Research Center

   9:30 - 10:00 Break

   10:00 - 12:00 Formal Verification and Theorem Proving (Chair: Ben Hocking)

• Hendrik Maarand and Tarmo Uustalu Certified Foata Normalization for Generalized Traces
• Ansgar Fehnker, Kaylash Chaudhary and Vinay Mehta An Even Better Approach - Improving the B.A.T.M.A.N. Protocol Through Formal Modelling and Analysis
• Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C
• Saksham Chand and Yanhong A. Liu Simpler Specifications and Easier Proofs of Distributed Algorithms Using History Variables

   12:00 - 1:30 Lunch

   1:30 - 3:00 Formal Methods and Autonomy (Chair: Julia Badger)

• Siddhartha Bhattacharyya, Thomas Eskridge, Natasha Neogi, Marco Carvalho and Milton Stafford Formal Assurance for Cooperative Intelligent Autonomous Agents
• Ruben Giaquinta, Ruth Hoffmann, Murray Ireland, Alice Miller, and Gethin Norman Strategy Synthesis for Autonomous Agents using PRISM
• Lola Masson, Jérémie Guiochet, Hélène Waeselynck, Martin Törngren, Sofia Cassel and Kalou Cabrera Tuning permissiveness of active safety monitors for autonomous systems

   3:00 - 3:30 Break

   3:30 - 5:30 Specification Frameworks (Chair: Kristin Rozier)

• Massimo Narizzano, Luca Pulina, Armando Tacchella and Simone Vuotto Consistency of Property Specification Patterns with Boolean and Constrained Numerical Signals
• Giovanna Broccia, Paolo Milazzo and Peter Csaba Ölveczky An Executable Formal Framework for Safety-Critical Human Multitasking
• Sarah Benyagoub, Meriem Ouederni, Yamine Ait Ameur and Atif Mashkoor Incremental Construction of Realizable Choreographies
• Flavio M. de Paula, Arvind Haran and Brad Bingham An Efficient Rewriting Framework for Trace Coverage of Symmetric Systems

DAY 2: April 18, 2018 (Wednesday)

   8:00 - 8:30 Registration

   8:30 - 9:30 Invited Talk (Chair: César Muñoz)

• Gilles Dowek (INRIA, CNRS, ENS Paris-Saclay, France).Formal Methods: A Plea for Knowing What Computers Do

   9:30 - 10:00 Break

   10:00 - 12:00 Symbolic Execution and Testing (Chair: Ivan Perez)

• Miguel Romero and Camilo Rocha Symbolic Execution and Reachability Analysis using Rewriting Modulo SMT for Spatial Concurrent Constraint Systems with Extrusion
• Rui Qiu, Sarfraz Khurshid, Corina Pasareanu, Junye Wen and Guowei Yang Using Test Ranges to Improve Symbolic Execution
• Marcus Gerhold, Arnd Hartmanns and Mariëlle Stoelinga Model-Based Testing for General Stochastic Time
• César Augusto Ochoa Escudero, Rémi Delmas, Thomas Bochot, Matthieu David and Virginie Wiels Automatic Generation of DO-178 Test Procedures

   12:00 - 1:30 Lunch

   1:30 - 3:15 Formal Methods in Emergent Technologies (Chair: Sofiène Tahar)

• Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan and Ashish Tiwari Output Range Analysis for Deep Feedforward Neural Networks
• Francesco Marconi, Giovanni Quattrocchi, Luciano Baresi, Marcello M. Bersani and Matteo Rossi On the Timed Analysis of Big-Data Applications
• Ansgar Fehnker and Kaylash Chaudhary Twenty Percent and a Few Days - Optimising a Bitcoin Majority Attack (short paper)
• Cumhur Erkan Tuncali, Bardh Hoxha, Guohui Ding, Georgios Fainekos and Sriram Sankaranarayanan Experience Report: Application of Falsification Methods on the UxAS System (short paper)
• Marco A. Feliú and Mariano Moscato Towards a Formal Safety Framework for Trajectories (short paper)

   3:15 - 3:45 Break

   3:45 - 5:30 Model Checking I (Chair: Mahyar Malekpour)

• Bruno Dutertre, Dejan Jovanović and Jorge Navas Verification of Fault-Tolerant Protocols with Sally (short paper)
• Philipp Koerner and Jens Bendisposto Distributed Model Checking Using ProB
• Radha Nakade, Eric Mercer, Peter Aldous and Jay McCarthy Model-checking Task Parallel Programs for Data-race
• Alfons Laarman Optimal Storage of Combinatorial State Spaces

DAY 3: April 19, 2018 (Thursday)

   8:00 - 8:30 Registration

   8:30 - 9:15 Static Analysis (Chair: Alwyn Goodloe)

• Aymeric Fromherz, Abdelraouf Ouadjaout and Antoine Miné Static Value Analysis of Python Programs by Abstract Interpretation
• Zhuo Chen and Werner Dietl Don't Miss the End: Preventing Unsafe End-of-File Comparisons (short paper)

   9:15 - 9:30 Tools (Chair: Alwyn Goodloe)

• András Vörös, Márton Búr, István Ráth, Ákos Horváth, Zoltán Micskei, László Balogh, Bálint Hegyi, Benedek Horváth, Zsolt Mázló and Dániel Varró MoDeS3: Model-based Demonstrator for Smart and Safe Cyber-Physical Systems (short paper)

   9:30 - 10:00 Break

   10:00 - 11:45 Model Checking II (Chair: Frédéric Loulergue)

• Alfons Laarman Stubborn Transaction Reduction
• Jeroen Meijer and Jaco van de Pol Sound Black-Box Checking in the LearnLib
• Yassmeen Elderhalli, Osman Hasan, Waqar Ahmad and Sofiène Tahar Formal Dynamic Fault Trees Analysis using an Integration of Theorem Proving and Model Checking
• Andrew Ireland, Maria Teresa Llano and Simon Colton The Use of Automated Theory Formation in Support of Hazard Analysis (short paper)

   11:45 - 12:00 Business Meeting (Chair: César Muñoz)