The Research Ideas of FMICS-AVoCS 2016 are available as Technical Report 2016-TR-010, Istituto di Scienza e Tecnologie dell'Informazione, Consiglio Nazionale delle Ricerche, 2016.
The Proceedings of FMICS-AVoCS 2016 are available from Springer as LNCS 9933.

The workshop takes place in rooms C29 (presentations) and C40 (registration and coffee breaks). Click here for information on how to get to the workshop rooms. If you need assistance, please call +39 050 6212881 (C29) or +39 050 6212991 (C40).

Monday 26 September
      KEYNOTE 1 (chair: Stefania Gnesi)
14:30 15:30   Silvia Mazzini: Lessons Learned in a Journey Toward Correct-by-Construction Model-Based Development
15:30 16:00   COFFEE BREAK
      SESSION 1 (chair: Diego Latella)
      Automated Verification Techniques 1
16:00 16:30   Christian Dernehl, Norman Hansen and Stefan Kowalewski:  Abstract Interpretation of MATLAB Code with Interval Sets
16:30 17:00   Hadrien Bride, Olga Kouchnarenko, Fabien Peureux and Guillaume Voiron: Workflow Nets Verification: SMT or CLP?
17:00 17:30   Mahmoud Mohsen and Bart Jacobs: One Step Towards Automatic Inference of Formal Specification Using Automated VeriFast
19:00 22:00   WELCOME RECEPTION at the Museum of Computing Machinery (Maps)
      Pisa is the birthplace of Italian computer science. It is in Pisa that the first Italian computers (Olivetti) were designed in the 50s and in 1969 the first Master
      in Informatics was established at the University of Pisa. The Museo degli Strumenti per il Calcolo (Museum of Computing Machinery) showcases artefacts
      from the early days of Italian computer science and a selection of personal computing machines.
Tuesday 27 September
09:00 09:30   REGISTRATION
      KEYNOTE 2 (chair: Alexander Knapp)
09:30 10:30   Jan Peleska: Model-based Testing Strategies and Their (In)dependence on Syntactic Model Representations
10:30 11:00   COFFEE BREAK
      SESSION 2 (chair: Jaco van de Pol)
      Automated Verification Techniques 2
11:00 11:30   Takuro Kutsuna and Yoshinao Ishii: Analyzing Unsatatisfiability in Bounded Model Checking using Max-SMT and Dual Slicing
11:30 12:00   Yu Lu, Alice A. Miller, Ruth Hoffmann and Christopher W. Johnson: Towards the Automated Verification of Weibull Distributions for System Failure Rates
12:00 12:30   Axel Habermaier, Alexander Knapp, Johannes Leupolz and Wolfgang Reif: Fault-Aware Modeling and Specification for Efficient Formal Safety Analysis
12:30 14:00   LUNCH
      SESSION 3 (chair: Markus Roggenbach)
      Research Ideas on Automated Verification Techniques
14:00 14:20   Arnd Hartmanns, Sybe van Hijum, Jeroen Meijer and Jaco van de Pol: Towards Multi-Core Symbolic Model Checking of Timed Automata
14:20 14:40   Laure Petrucci and Jaco van de Pol: Parametric Interval Markov Chains: Synthesis Revisited
      Research Ideas on Model-based System Analysis
14:40 15:00   Paolo Milazzo, Giovanni Pardini and Giovanna Broccia: Towards a High-Level Model Checking Language: Object-orientation, Data Structures and Local Variable Pruning 
      Model-based System Analysis 1
15:00 15:30   Arnaud Dieumegard, Andres Toom and Marc Pantel: Block Library Driven Translation Validation for Dataflow Models in Safety Critical Systems 
15:30 16:00   COFFEE BREAK
      SESSION 4 (chair: Paolo Milazzo)
      Model-based System Analysis 2
16:00 16:30   Mounir Chadli, Jin Hyun Kim, Axel Legay, Louis-Marie Traonouez, Stefan Naujokat, Bernhard Steffen and Kim Guldstrand Larsen:
      A Model-Based Framework for the Specification and Analysis of Hierarchical Scheduling Systems
16:30 17:00   Irina Mariuca Asavoae, Hoang Nga Nguyen, Markus Roggenbach and Siraj Shaikh: Utilizing K Semantics for Collusion Detection in Android Applications
17:00 17:30   Axel Habermaier, Johannes Leupolz and Wolfgang Reif: Unified Simulation, Visualization, and Formal Analysis of Safety-Critical Systems with S#
20:00 23:00   SOCIAL DINNER at the trattoria Al Signor Mimmo (Maps)
Wednesday 28 September
      KEYNOTE 3 (chair: Maurice ter Beek)
 9:30  10:30   Thomas Arts: Random Testing of Formal Properties for Industrial Critical Systems
10:30 11:00   COFFEE BREAK
      SESSION 5 (chair: Alessandro Fantechi)
      Applications and Case Studies 1
11:00 11:30   Ning Ge, Eric Jenn, Nicolas Breton and Yoann Fonteneau: Formal Verification of a Rover Anti-collision System
11:30 12:00   Steffen Beringer and Heike Wehrheim: Verification of AUTOSAR Software Architectures with Timed Automata
12:00 12:30   Philip Johnson-Freyd, Geoffrey C. Hulette and Zena M. Ariola: Verification by Way of Refinement: 
      A Case Study in the Use of Coq and TLA in the Design of a High Consequence System
12:30 14:00   LUNCH
      SESSION 6 (chair: Louis-Marie Traonouez)
      Applications and Case Studies 2
14:00 14:30   Somsak Vanit-Anunchai: Application of Coloured Petri Nets in Modelling and Simulating a Railway Signalling System
14:30 15:00   Alessandro Fantechi: Formal Techniques for a Data-Driven Certification of Advanced Railway Signalling Systems
      Research Ideas on Applications and Case Studies
15:00 15:20   Luca Geretti, Davide Bresolin and Tiziano Villa: Formal verification of non-linear hybrid systems using Ariadne
15:20 15:40   Josh Taylor, Alexander Knapp, Markus Roggenbach and Holger Schlingloff: Automation of test case assessment in SPLs – experiences and open questions