Report by Ridhi Jain (IIIT Delhi, India)
The sixth Conference on Formal Methods in Software Engineering, FormaliSE 2018, was organized as a one-day event in Gothenburg, Sweden on 2nd June. The event was attended by roughly 50 researchers, including people from industry as well as academia in the area of Formal Verification from around the globe.
The crowd at FormaliSE 2018.
The session began with a welcome to the FormaliSE community by PC co-chairs Paola Spoletini and Patrizio Pelliccione, followed by a keynote given by Mariëlle Stoelinga (Radboud University Nijmegen & University of Twente, the Netherlands).
Keynote speaker Mariëlle Stoelinga.
The event was further divided into five sessions.
Session 1: Formal Methods for Autonomous Systems
The session chair, Claudio Menghi, Postdoc at University of Göteborg guided the audience towards the only talk of the session on Formal Verification of Complex Robotic Systems on Resource-Constrained Platforms. The session was about verifying the behavioral and timed properties of robotic systems.
Session 2: Runtime Verification
The session was chaired by Domenico Bianculli from Software Verification and Validation Lab, University of Luxembourg. It had three presentations aligned with the topic Runtime Verification. The first one was an overview of Specification Patterns for Verification of Parametric Traces and extending them. The second was about Runtime Verification of Hyperproperties for Deterministic Programs and the last presentation was on Testing Meets Static and Runtime Verification.
Session 3: Student presentations
The third session, chaired by Nico Plat was a bit different from the others. Four students from different Universities from around the world presented their works in “Pecha Kucha” format.
Session 4: Program Verification and Application
The session chair, Wolfgang Ahrendt, Associate Professor at Chalmers University of Technology drove the session. The session consisted three presentations on Program Verification and Application. The first presentation was about translating CIL to Java-bytecode to leverage the existing mature and sound Java-bytecode analyzers on CIL. This paper won the FormaliSE 2018 “Distinguished Paper Award”. The second presentation was about Modeling Time for Automatic Error Detection in Java Programs and the last talk of the session was about Domain-specific Design of Patient Classification in Cancer-related Cachexia Research.
Distinguished paper award: Pietro Ferrara, Agostino Cortesi and Spoto Fausto
Session 5: Formal Methods for Autonomous Systems
The last session of the event was chaired by Michael Whalen, Director of the University of Minnesota Software Engineering Center. It had three presentations on the topic Formal Methods for Autonomous Systems. The first one was on Self-Adaptive Automata on autonomous vehicles for searching. The second talk was about Formal Verification of an Autonomous Wheel Loader by Model Checking which provides the timed automata description of the vehicle’s control system, including the abstracted path planning and collision avoidance algorithms. The last talk of the session was about Formal verification of automotive embedded software that proposes an approach introducing formal methods into the development of automotive embedded software.
Closing Remarks
After the successful completion of event, the General Chairs, Stefania Gnesi and Nico Plat expressed their gratitude to all the participants, session chairs and presenters. Finally, the event ended with leaving the audience motivated to produce high quality research in the field of Formal Methods.
More information
For more information on the event see www.formalise.org.