Report on the first two days of SOFSEM 2017 (guest post by Ignacio Fábregas)

Ignacio Fábregas has kindly sent me this report on the first two days of SOFSEM 2017, which is being held this week in Limerick, Ireland. I hope you'll enjoy reading it.  Many thanks to Ignacio for agreeing to write this guest post.

 

SOFSEM has always be an atypical conference with a format closest to a Winter School. This year marks a new beginning for the SOFSEM conference, since it's the first time it's held outside the Czech Republic or the Slovak Republic. As Jan van Leeuwen told us in the Welcome Reception on Monday, the goal of the Steering Committee of SOFSEM is to keep the spirit of SOFSEM alive while moving to a more typical format for a computer science conference. The main ingredients are still there: the keynote talks of renowned experts, tutorial sessions and the Student Research Forum; the only main difference is the country (Ireland) and the schedule (instead of having all the keynote talks the first and last day, now they are distributed across the conference days).

The first day of the Conference the keynote speaker was Kim G. Larsen. He told us about Cyber-Physical Systems (CPS), that is, systems combining computing elements with dedicated hardware and software having to monitor and control a particular physical environment. In order to study them, Larsen and his team propose a model-based approach, powered by the use of the tool Uppaal. An example of CPS is the adaptive cruise control for cars, an application where Europe is trying to match U.S. (where the Google Self-Driving car has already been approved by the legislation in several U.S. states) and where the team of Kim Larsen is making advances.

After the keynote talk we had the first parallel sessions: two sessions of the Foundations of Computer Science (FOCS) track and the first tutorial. I went to the FOCS session about Semantics, Specification and Compositionality, mainly because my talk was there :) But, more importantly, there was a talk of Uli Fahrenberg and another by Linda Bordo. Uli talked about behavioural specification theories for most equivalences in the linear-time–branching-time spectrum. He humbly defined his work as "almost" a rewriting of some old and overlooked results. Going back, reading and, most importantly, understanding, old results is a non-trivial exercise that computer science researchers should do more often. On the other hand, Linda talked about link-calculus, as a model that extends the point-to-point communication discipline of Milner’s CCS with multiparty interactions. She used links to build chains describing the flow of information among the agents participating in that interaction. The difficult part comes when deciding both the number of participants in an interaction and how they synchronize.

The second day of conference we had two keynote talks. Axel Legay talked about Software Product Lines (SPL), that is, the families of similar software products built from a common set of features. For example, like the mobile phones that a company as Samsung or HTC produce. He showed us how he and his team formalizes SPLs by means of what they called Featured Transition Systems and how the designed verification algorithms and tools to check temporal properties over them. The second keynote talk was by Marjan Mernik. He told us about Domain-Specific Languages that assist software developers in programming, and some open problems in the field like the lacking of tool support for different Domain-Specific Languages and the difficulties combining them.

Relative to the conference papers, in the FOCS session in Verification and Automated System Analysis we have talks by Mohammad Reza Mousavi, Nataliya Gribovskaya, Zhaowei Xu and Saket Saurabh. I want to highlight Mohammad's talk about the complexity of deriving invertible sequences from finite-state machines. The problem is the following: checking the existence of input/output sequences (UIOs) that identify states of the finite state machine specification (as it's the case of ioco) is PSPACE-complete; so some UIO generation algorithms utilise what are called invertible sequences; these allow one to construct additional UIOs once a UIO has been found. Mohammad and his coauthors studied some optimization problems and their complexity.

And that's all for now. Tomorrow (18 January 2017) we'll have fewer talks since we have the excursion and conference dinner. Also I'm planning to go for one tutorial session by Andrew Butterfield. I'll tell you more on that.