08:30: Welcome

08:35: Session 1 - Security analysis

  • A Model for Provably Secure Software DesignAlexander van den Berghe, Koen Yskout, Riccardo Scandariato and Wouter Joosen. KU Leuven (Belgium), and University of Gothenburg (Sweden).
  • Verifying the Reliability of Operating System-Level Information Flow Control Systems in Linux. Laurent Georget, Mathieu Jaume, Guillaume Piolle, Frédéric Tronel and Valérie Viet Triem. Université de Rennes (France), and Sorbonne Universités (France).


09:30: Session 2 - Security verification

  • Trusted and Tooled Approach to Design a Network Monitor.  Koichi Shimizu, Teruyoshi Yamaguchi, Tsunato Nakai, Takeshi Ueda, Nobuhiro Kobayashi and Benoît Boyer. Mitsubishi Electric (Japan and France).
  • Model Checking for Mobile Android Malware Evolution. Fabio Martinelli, Francesco Mercaldo, Vittoria Nardone, Antonella Santone, Gigliola Vaglini and Aniello Cimitile. IIT-CNR (Italy), University of Sannio (Italy), and University of Pisa (Italy).


10:30: Coffee break
During the break there will be poster sessions/brief presentations.

11:00: Keynote presentation: Efficient SAT-Based Software Analysis: from Automated Testing to Automated Verification and Repair (abstract). Nazareno Aguirre. University of Rio Cuarto and CONICET (Argentina).

12:00: Session 3 - Requirements

  • Using BDD and SBVR to refine business goals into an Event-B model: a research idea. Fábio Levy Siqueira, Thiago C. De Sousa and Paulo Sergio Muniz Silva. Universidade de Sao Paulo (Brazil), and Universidade Estadual do Piaui (Brazil). 


12:30: Lunch

14:00: Session 4 - Quantitive modeling and analysis

  • Modeling Families of Public Licensing Services: A Case Study. Guillermina Cledou and Luis Barbosa. HASLab INESCTEC & Universidade do Minho (Portugal).
  • Formal Verification of ROS-based Robotic Applications using Timed-Automata. Raju Halder, Jose Proenca, Nuno Macedo and Andre Santos. Indian Institute of Technology Patna (India), and HASLab INESCTEC & Universidade do Minho (Portugal).
  • Featured Weighted Automata. Uli Fahrenberg and Axel Legay. École polytechnique Palaiseau (France), and Inria Rennes (France).


15:30: Tea break
During the break there will be poster sessions/brief presentations.

16:00: Session 5 - Verification and testing

  • Correct Safety Critical Hardware Descriptions via Static Analysis and Theorem Proving. Nicholas Moore and Mark Lawford. McMaster University (Canada).
  • A Generic Algorithm for Program Repair. Besma Khaireddine, Aleksandr Zakharchenko and Ali Mili. NJIT (USA).
  • Partition-based Coverage Metrics and Type-guided Search in Concolic Testing for JavaScript Applications. Sora Bae, Joonyoung Park and Sukyoung Ryu. KAIST (Korea). 


17:30: End of workshop