FormaliSE 2013

The first edition of FormaliSE was held on Saturday 25 May 2013, San Francisco (USA), co-located with ICSE 2013. About 30 participants heard an inspiring invited lecture given by Alan Wassyng of McMaster University, Canada. Alan’s extensive experience as both an engineering practitioner, and as a formal methods researcher, has led him to question the goals of formal methods research and the seriousness with which the needs of the profession are treated by researchers.

Nine scientific papers were accepted from 25 submissions reviewed by the international programme committee. (36% acceptance rate). Each paper was reviewed by 4 PC members and the average rating was high compared to normal standards. Topics ranged from verification to the methodology of collaborative development. A “round table” discussion, chaired by John Fitzgerald of FME, concluded the workshop.

Proceedings

The proceedings of the workshop were published as part of the ICSE 2013 proceedings. A table of contents including brief abstracts can be found here, and the proceedings themselves can be found here.

Programme

8:30-8:45: Welcome: Introduction to FormaliSE by Stefania Gnesi and Nico Plat

8:45-9:30: Invited keynote: Though this be madness, yet there is method in it? Alan Wassyng (McMaster University, Canada) (slides)

Abstract: After decades of research, and despite significant advancement, formal methods are still not widely used in industrial software development. Industry practitioners believe that the methods and tools coming out of academia are, to a large extent, irrelevant and ineffective in tackling real-life projects. They are difficult to use, esoteric, and do not scale (at all). This paper reflects more than twenty years spent in first experiencing the problems in industry, and then struggling to do something about it in academia. We present some examples of formal method madness/blindness, as well as a few successes. We believe the problem is deep. To start to address it and make progress in producing methods that are truly usable in industry, and rigorous enough to make them effective engineering methods, we need to reconsider the role of computer scientists, software engineers, software developers, as well as the hurdles to promotion for academics. Along the way, the paper will present a few fundamental principles that we think spell the difference between success and failure in producing usable formal methods, and convincing software professionals in industry to adopt them.

9:30-10:30. Session 1: Specification

Paper presentation: Lightweight Formal Models of Software Weaknesses Robin Gandhi, Harvey Siy and Yan Wu (University of Nebraska at Omaha, USA)

Paper presentation: Do You Speak Z? Formal Methods under the Perspective of a Cross-Cultural Adaptation Problem Andreas Bollin (Alpen-Adria Universitat, Austria) 10:30-11:00:

Break

11:00-12:30. Session 2: Verification

Paper presentation: Functional SMT solving with Z3 and Racket Siddharth Agarwal and Amey Karkare (Indian Institute of Technology Kanpur, India)

Paper presentation: Trace Based Reachability Verification for Statecharts Kumar Madhukar, Ravindra Metta, Ulka Shrotri and R. Venkatesh (Tata Consultancy Services, India)

Paper presentation: An Integrated Data Model Verifier with Property Templates Jaideep Nijjar, Ivan Bocic and Tevfik Bultan (University of California at Santa Barbera, USA) 12:30-14:00:

Lunch

14:00-15:00. Session 3: Application of Formal Methods

Paper presentation: Towards a Formalism-Based Toolkit for Automotive Applications Rainer Gmehlich, Katrin Grau, Felix Loesch, Alexei Iliasov, Michael Jackson and Manuel Mazzara

Paper presentation: Recommendations for Improving the Usability of Formal Methods for Product Lines Joanne M. Atlee, Sandy Beidu, Nancy A. Day, Fathiyeh Faghih and Pourya Shaker (University of Waterloo, Canada)

15:00-16:00. Session 4: Timed Systems

Paper presentation: Automatic Validation of Infinite Real-Time Systems Thomas Göthel and Sabine Glesner (Technische Universitat Berlin, Germany)

Paper presentation: A framework for the rigorous design of highly adaptive timed systems Louis-Marie Traonouez, Axel Legay, Maxime Cordy and Pierre-Yves Schobbens (University of Namur, Belgium, and INRIA Rennes, France)

Break

16:30-18:00: Round table discussion (summary)

Programme Committee

  • Yamine Ait-Ameur (IRIT/ENSEEIHT, France)
  • Manfred Broy (Technical University München, Germany)
  • Jürgen Dingel (Queen's University, Canada)
  • Cindy Eisner (IBM Haifa Research Laboratory, Israel)
  • Arie Gurfinkel (Carnegie Mellon University, USA)
  • Patrick Heymans (University of Namur, Belgium, and INRIA, France)
  • Alessandro Fantechi (University of Florence, Italy)
  • Connie Heitmeyer (Naval Research Laboratory, USA)
  • Mike Hinchey (Lero, Ireland)
  • Axel van Lamsweerde (University of Louvain. Belgium)
  • Peter Gorm Larsen (Aarhus University, Denmark)
  • Marc Lawford (MacMaster University, Canada)
  • Thierry Lecomte (ClearSy, France)
  • Yves Ledru (IMAG, France)
  • Antónia Lopes (University of Lisbon, Portugal)
  • Tiziana Margaria (Potsdam University, Germany)
  • Henry Muccini (Universita degli Studi dell’Aquila, Italy)
  • Isabelle Perseil (Inserm, France)
  • Steve Riddle (University of Newcastle, UK)
  • Matteo Rossi (Politecnico di Milano, Italy)
  • Wolfram Schulte (Microsoft, USA)
  • Elena Troubitsyna (Abo University, Finland)
  • Sebastián Uchitel (Imperial College and Universidad de Buenos Aires, UK and Argentina)
  • Willem Visser (University of Stellenbosch, South Africa)
  • Fatiha Zaïdi (LRI/CNRS, France)

Organizing Committee

Organizing Committee members and PC Chairs for FormaliSE 2013 were:

Nico Plat and Stefania Gnesi