FormaliSE 2017 group photo

08:30: Welcome [slides]

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) [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]


12:30: Lunch

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].
  • Partition-based Coverage Metrics and Type-guided Search in Concolic Testing for JavaScript Applications. Sora Bae, Joonyoung Park and Sukyoung Ryu. KAIST (Korea) [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