FormaliSE 2017

The 5th edition of FormaliSE was held on Saturday 27 May in Buenos Aires (Argentina), co-located with ICSE 2017. 30 Participants heard an inspiring keynote by Nazareno Aguirre (University of Rio Cuarto and CONICET), mixed with presentations of scientific papers, including discussions. 

Eleven scientific papers were accepted from 22 submissions that were reviewed by an international programme committee (50% acceptance rate). Each paper was reviewed by 3 PC members.

Proceedings

The proceedings of the workshop were published as part of the ICSE 2017 Workshop Proceedings in the ACM and IEEE Digital Libraries.

Programme

FormaliSE 2017 group photo

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

 

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].

 

Programme Committee

  • Gustavo Betarte (Universidad de la República, Uruguay)
  • Andreas Bollin (University of Klagenfurt, Austria)
  • Christiano Braga (Universidade Federal Fluminense, Brasil)
  • Ana Cavalcanti (University of York, UK)
  • Nicolas D'Ippolito (Universidad de Buenos Aires, Argentina)
  • Nancy Day (University of Waterloo, Canada)
  • Ben Di Vito (NASA Langley Research Center, USA)
  • Alessandro Fantechi (Universita' di Firenze, Italy)
  • Antonio Filieri (Imperial College London, UK)
  • Stefania Gnesi (ISTI-CNR, Italy) (Chair)
  • Jan Friso Groote (Eindhoven University of Technology, The Netherlands)
  • Peter Gorm Larsen (Aarhus University, Denmark)
  • Mark Lawford (McMaster University, Canada)
  • Thierry Lecomte (ClearSy, France)
  • Yves Ledru (Université Joseph Fourier, France)
  • Axel Legay (IRISA/INRIA, France)
  • Malte Lochau (TU Darmstadt, Germany)
  • Hernán Melgratti (University of Buenos Aires, Argentina) (Chair)
  • Ravindra Metta (TCS, India)
  • Tomohiro Oda (Software Research Associates Inc., Japan)
  • Liliana Pasquale (Lero, Ireland)
  • Patrizio Pelliccione (Chalmers University of Technology and University of Gothenburg, Sweden)
  • Ken Pierce (Newcastle University, UK)
  • Nico Plat (Thanos, The Netherlands) (Chair)
  • Sanjai Rayadurgam (University of Minnesota, USA)
  • Matteo Rossi (Politecnico di Milano, Italy)
  • Thomas Santen (Technical University of Berlin, Germany)
  • Antonella Santone (University of Sannio, Italy)
  • Laura Semini (University of Pisa, Italy)
  • Marjan Sirjani (Reykjavik University, Iceland)
  • Paola Spoletini (Kennesaw State University, USA)
  • Jun Sun (Singapore University of Technology and Design, Singapore)
  • Marcel Verhoef (European Space Agency, The Netherlands)

 

Organizing Committee

Organizing Committee members and PC Chairs for FormaliSE 2017:

Share