Formalise 2015

The third edition of FormaliSE was held on Monday 18 May in Florence (Italy), co-located with ICSE 2015. 35 Participants heard inspiring keynotes by Dino Mandrioli (Polytechnico di Milano, Italy) and John Fitzgerald (Newcastle University, UK), mixed with presentations of scientific papers, including discussions. A panel discussion, chaired by Nico Plat and Stefania Gnesi, concluded the workshop. Dino Mandrioli, John Fitzgerald, Alessandro Fantechi and Pamela Zave were the panel members.

Nine scientific papers were accepted from 27 submissions that were reviewed by an international programme committee (33% acceptance rate). Each paper was reviewed by 3 PC members and the average rating was high compared to normal standards. Topics ranged from security aspects of formal methods, to verification and to cyber physical systems. 

Participants of FormaliSE 2015

Proceedings

The proceedings of the workshop were published as part of the ICSE 2015 proceedings (IEEE publication).

Programme

08:40 to 08:45: Introduction

  • Nico Plat and Stefania Gnesi. "Welcome to FormaliSE 2015" (slides)

08:45 to 09:30: Keynote

  • Dino Mandrioli. “On the Heroism of really Pursuing Formal Methods” (slides)

09:30 to 10:30: Security

  • Yves Ledru, Akram Idani and Jean-Luc Richier. “Validation of a security policy by the test of its formal B specification - a case study” (slides)
  • Noomene Ben Henda, Karl Norrman and Katharina Pfeffer. “Formal Verification of the Security for Dual Connectivity in LTE” (slides)

10:30 to 11:00: Break

11:00 to 12:30: Exploratory Applications

  • Jo Atlee, Uli Fahrenberg and Axel Legay. “Measuring Behaviour Interactions between Product-Line Features” (slides)
  • Michele Ceccarelli, Luigi Cerulo, Giuseppe De Ruvo, Vittoria Nardone and Antonella Santone. “Infer Gene   Regulatory Networks from Time Series Data with Probabilistic Model Checking” (slides)
  • Tomohiro Oda, Keijiro Araki and Peter Gorm Larsen. “VDMPad: a Lightweight IDE for Exploratory VDM-SL Specification” (slides)

12:30 to 13:44: Lunch

13:45 to 14:30: Keynote

  • John Fitzgerald. "Cyber-Physical System Design: Formal Foundations, Methods and Integrated Toolchains” (slides)

14:30 to 15:30: Cyber Physical Systems

  • Monika Bialy, Mark Lawford, Vera Pantelic and Alan Wassyng. “A Methodology for the Simplification of Tabular Designs in Model-Based Development" (slides)
  • Constance Heitmeyer and Elizabeth Leonard. “Obtaining Trust in Autonomous Systems: Tools for Formal Model Synthesis and Validation” (slides)

15:30 to 16:00: Break

16:00 to 17:00: Program verification

  • Guillaume Claret and Yann Régis-Gianas. “Mechanical verification of interactive programs specified by use cases” (slides)
  • Domenico Bianculli, Antonio Filieri, Carlo Ghezzi, Dino Mandrioli and Alessandro Maria Rizzi. “Syntax-driven Program Verification of Matching Logic Properties” (slides)

17:00 to 18:00: Panel discussion

Programme Committee

  • Keijiro Araki (Kyushu University, Japan)
  • Andreas Bollin (Klagenfurt University, Austria)
  • Manfred Broy (Technical University of Munich, Germany)
  • Ana Cavalcanti (York University, UK)
  • Roderick Chapman (Protean Code Ltd, UK)
  • Nancy Day (University of Waterloo, Canada)
  • Ewen Denney (SGT/NASA Ames, United States)
  • Cindy Eisner (IBM Haifa Research Laboratory, Israel) 
  • Alessandro Fantechi (University of Florence, Italy)
  • Antonio Filieri (Universität Stuttgart Germany)
  • Jan Friso Groote (Eindhoven University of Technology, The Netherlands)
  • Mats P.E. Heimdahl, (University of Minnesota, USA).
  • Claire Ingram (Newcastle University, UK)
  • Nicolas D'Ippolito (Universidad de Buenos Aires, Argentina)
  • Peter Gorm Larsen (Aarhus University, Denmark)
  • Marc Lawford (MacMaster University, Canada)
  • Thierry Lecomte (ClearSy, France)
  • Yves Ledru (IMAG, France)
  • Axel Legay (INRIA Rennes, France)
  • Antónia Lopes (University of Lisbon, Portugal)
  • Tiziana Margaria (University of Limerick and Lero, Ireland)
  • Ravidra Metta (Tata Consultancy Services, India)
  • Henry Muccini (Universita degli Studi dell’Aquila, Italy)
  • Matteo Rossi (Politecnico di Milano, Italy)
  • Thomas Santen (Microsoft, UK)
  • Laura Semini (Pisa University, Italy)
  • Marjan Sirjani, (Reykjavik University, Iceland)

Organizing Committee

Organizing Committee members and PC Chairs for FormaliSE 2015:

 

Stefania Gnesi and Nico Plat