I recently took my first work trip in my new job (which may be a personal record, since I’ve only working there for six weeks!) to run the workshop that I organise, FMAS, and attend the conference we held this year’s edition of the workshop at, iFM.

Both FMAS and iFM were held in Leiden, in The Netherlands. This was my first time visiting The Netherlands, I’ve had connecting flights through Schiphol Airport many times but I’ve never left the airport – sometimes for a very, very long time. I took the train from the airport to Leiden, and it arrived on time, was cheap, and the ride was very smooth. However, as a Brit, I have a pretty low bar for trains being good!

The other obvious observation is: bikes. There were a lot of bicycles, living up to the stereotype, and a lot of fantastic bicycling infrastructure. There were bicycle racks all over the place, lots of people cycling with kids (presumably to school) even in rainy weather, and lots of cycle lanes that were separated from the road. there was even a specific underpass for the cycle lane. It just felt so…modern, in a nice way.

Picture of the view from my room

After I arrived, I spent some time reviewing a few papers. Now, it was a Sunday so I would in general say that this was bad. But I hadn’t had time to review them before and knew I wouldn’t after I got back, so I chose to use some of that time on work.

Then I went downstairs to get dinner and ran into a work friend (I wonder why they were in Leiden…) so I got to have dinner and a beer, and catch up. This was a friend who I had so far only seen on work video calls, so it was really nice to see them in person. They also revealed that they have read some of these posts and said some nice things about them (Hi Mengwei!) so that was lovely.

Picture of a windmill in Leiden

integrated Formal Methods (iFM 23)

As I have said before, and will probably say again, I think that iFM is my favourite formal methods conference. I generally find that the mixture of work that is sent there is interesting, often with a more practical flavour, which I like. I’ve previously said that it’s the conference’s focus on integration of formal and/or non-formal methods that gives it such an interesting feel, but I mentioned this to someone this year (someone in a position to know) and they said that the integrated part of the conference’s scope has slowly waned over the years. I can see this point, right at the beginning the conference about about integrating formal methods – mushing them together to tackle both data and behaviour, for example. But I think that the broadening/loosening of the scope (to include integrating formal and non-formal methods) still works and brings in the interesting practical work that I like. Of course, that could all just be an explanation I’ve constructed to support my original idea!

That ramble aside, the conference was good fun. The venue used to be a textiles factory, so it had a trendy, post-industrial feel – it could have been a hipster bar.

Picture of the inside of the conference venue.

When I’m at a conference, I tend to not see very much of the city I’m in. The most obvious opportunity for a little sight-seeing is while heading to whatever social event/dinner might have been organised. While walking to dinner, I managed to get a few snaps. Leiden seemed to be preparing for Christmas, so parts of the city centre were lit up and looking fantastic.

Picture of the city centre of Leiden with lit-up decorations seen over the canal.

The conference had a nice programme and it had a joint session with FMAS, which seemed to be useful for both us and iFM. We picked two papers from iFM for the joint session, both of which were a great complement for the programme at our own workshop:

  • A Formal Modelling and Analysis of a Self-Adaptive Robotic System by Juliane Päßler, Maurice H. ter Beek, Ferruccio Damiani, Silvia Lizeth Tapia Tarifa and Einar Broch Johnsen. doi: 10.1007/978-3-031-47705-8_18
  • CAN-verify: Verification Tool for BDI Agents by Mengwei Xu, Thibault Rivoalen, Blair Archibald and Michele Sevegnani. doi: 10.1007/978-3-031-47705-8_19

We, of course, had one of the FMAS papers in there, an interesting approach that uses model checking for roots planning their way out of dead ends:

  • Model checking for Robot Reactive Planning by Christopher Chandler, Bernd Porr, Alice Miller, and Giulia Lafratta. doi: 10.4204/EPTCS.395.6

And that was the end of iFM 2023, however FMAS 2023 still had another day to go. FMAS had started in the morning and this joint session was in the afternoon. So lets go back in time, for FMAS 2023.

Formal Methods for Autonomous Systems (FMAS 2023)

This was the fifth year that we had run FMAS, which felt like a big milestone for a small workshop started by two Research Associates in 2019. I felt quite proud that we had made it this far, from having seven submissions in 2019 to having 25 submissions this year.

My introduction to the workshop was slightly nostalgic, looking back on the four previous workshops and talking about what might be coming next. We had asked two colleagues, Maike Schwammberger and Mario Gleirscher, to join us in organising FMAS. This should help spread the workload and hopefully bring in some fresh ideas for the next five years of the workshop. I had only intended that they observe this year’s organising activities (I thought it was unfair to throw them in, mid-way through the cycle of organising the workshop) but they have been involved in lots of ways in the background this year, and I am very thankful for their help.

Picture of FMAS 2023 showing the audience

As I said, this year FMAS received 25 submissions and we accepted 15. We kept using the four paper types that we introduced for FMAS 2022 (which I had borrowed from the REFSQ conference, after we sent a paper there):

  • Vision papers describe directions for research into Formal Methods for Autonomous Systems;
  • Research previews describe well-defined research ideas that are in their early stages, and my not be fully developed yet. Work from PhD students is particularly welcome;
  • Experience report report on practical experiences in applying Formal Methods to Autonomous Systems, focussing on the experience and lessons to be learnt;
  • Regular papers describe completed applications of Formal Methods to an Autonomous System, new or improved approaches, evaluations of existing approaches, and so on.

The intention of these more explicit types of papers (as opposed to simply ‘long’ and ‘short’ papers) was to help authors convey to reviewers what their intention is with the paper, to avoid reviewers being too harsh on work that is not so novel (because it’s an Experience Report) or is describing early/unfinished work (because it’s a Research Preview). Hopefully they’re helpful, and not overly burdensome for the authors.

The proceedings are available via EPTCS at https://cgi.cse.unsw.edu.au/~eptcs/content.cgi?FMAS2023. There you can find the wonderful (even if I do say so myself) preface, the abstracts of the two invited talks, and the 15 papers. As an overview of what you can find in there, we had sessions themed around:

  • Trust and Information Flow,
  • Verification and Assurance of Neural Networks,
  • Verified Intelligent Transportation,
  • Formal Assurance across the Control Loop, and
  • Runtime verification.

And so FMAS is done for another year (although it’s not, because there are still some final things to do). But, FMAS Will Return…

We will be planning out how the workshop should look for the next five years, trying to make it more sustainable for us to continue working on and maybe add some more things to the programme. Best laid plans…