08:30: Welcome [slides]
08:35: Session 1 - Security analysis
- A Model for Provably Secure Software Design. Alexander van den Berghe, Koen Yskout, Riccardo Scandariato and Wouter Joosen. KU Leuven (Belgium), and University of Gothenburg (Sweden) [slides].
- 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) [slides].
09:30: Session 2 - Security verification
- A 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) [slides].
- 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) [slides].
10:30: Coffee break
with poster session: On the Three-way Interaction Optimizing Feature Based Systems Verification. Laura Semini, joint work with Alessandro Fantechi (University of Pisa, Italy) [slides].
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) [slides].
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) [slides]
14:00: Session 4 - Verification and testing
- Correct Safety Critical Hardware Descriptions via Static Analysis and Theorem Proving. Nicholas Moore and Mark Lawford. McMaster University (Canada) [slides].
- A Generic Algorithm for Program Repair. Besma Khaireddine, Aleksandr Zakharchenko and Ali Mili. NJIT (USA) [slides].
15:30: Tea break
16:00: Session 5 - Quantitive modeling and analysis
- Modeling Families of Public Licensing Services: A Case Study. Guillermina Cledou and Luis Barbosa. HASLab INESCTEC & Universidade do Minho (Portugal) [slides].
- 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) [slides].
- Featured Weighted Automata. Uli Fahrenberg and Axel Legay. École polytechnique Palaiseau (France), and Inria Rennes (France) [slides].
17:30: End of workshop