I continue my notes on this year's SOFSEM conference
where I left them.
On Wednesday, I attended the tutorial session by Andrew Butterfield on
Unifying Theories of Programming (UTP), a paradigm introduced by C.A.R.
Hoare. Broadly speaking, UTP combines denotational, operational and
algebraic semantics in a unified framework for both the formal
specification and implementation. It is almost as there was no distinction
between syntax and semantics. Andrew Butterfield also showed us his
tool UTP2, programmed in Haskell, and how the library for UTP in the
Isabelle theorem prover works.
One important
part in any conference is to be able to discuss with other colleagues
and experts about interesting papers. On Wednesday I missed the keynote
talk by Jakko Hollmen about Predictive Analytics because I was
talking about some papers with colleagues. (I found that to be a valid excuse to miss a
talk in a conference!) Also, on Wednesday we had the social programme:
an excursion with a guide around the city centre of Limerick and the
conference dinner in the Bunratty Castle. Inside the castle we not only
enjoyed a typical Irish dinner but also an entertainment program. It was
a dinner with a medieval flavour because of the place but also because
of the show we saw and the way we ate. We had a broth, pork ribs and
chicken... But without forks! So we ate with our hands while listening
to some typical Irish songs performed by the very talented people of the
Bunratty Castle.
That's not all that happened
on Wednesday. The organization had a surprise for us: since the lunch
break was two hours long, during the second hour we had a talk about
music and computers. Inside the Department of Computer Science in
Limerick there is the Digital Media & Arts Research Centre, and the
organization took advantage of this fact in order to propose them to
give 3 talks: one on Wednesday and two on Thursday. The first talk was
done by Mikael Fernström (
http://www.idc.ul.ie/mikael/)
, who explained us his work. He uses computers in order to produce new
sounds (frequencies that a physical instrument wouldn't be able to make)
and algorithms in order to create music for "things". As an example, he
created a piece that took some variables from meteorological data so we
could listen to how the weather in Ireland sounds.
On Thursday, in this special sessions, Giuseppe Torre (
http://www.muresearchlab.com/)
showed us his work, where he uses computers to represent art. For
example, his work 'AI PRISON' is a program in C++ that outputs '0'
unless the technological singularity in Kurzweil's sense (or
'Terminator' sense) appears. It is exposed in the BLITZ Contemporary Art
Gallery in Malta. Finally, Kerry l. Hagan (
http://www.kerrylhagan.net/)
played some of his musical works. Again, the use of computers is the cornerstone. She uses a program that allows her to program and compose
the music she is going to play. This three artistic sessions where a really
nice touch from the organization.
Back to the
science, on Thursday we started with a keynote talk by Óscar Pastor
López about Model-driven Development. The idea is that developers should
be freed from programming concerns and be able to concentrate on
guaranteeing that the final software product corresponds to what the
company asked for. There are two basic notions in this field: capability
and the Model Driven Architecture. The first one is especially used at
the earliest steps of a software process in order to characterize the
relevant modelling components to be specified. Whereas the Model Driven
Architecture is used in the definition of the desired software process
in order to structure the development from requirements to code.
Afterwards
I attended the tutorial by Cristina Seceleanu about verification and
test-case generation for Automotive Systems. Nowadays a car is developed
with more electric components than hydraulic ones. For example, the
connection between the steering wheel and the steering control is done
by wires and software. This makes mandatory the use of testing in order
to verify the correct behaviour of a car. In this field of research
tools as UPPAAL are of great use. After the lunch we had the second
keynote talk of the day. Paul Spirakis explained us about "programmable
matter", which at the beginning seemed a field closest to sci-fi than
actual computer science. So, let me explain what I understood, nowadays
digital information (as internet) has spread along the world. That
information is simply data, which can be manipulated. This vision is
focused in our ability to manipulate data, and thus extended to
manipulate matter via information-theoretic and computing mechanisms,
incorporating information to the physical world. This is inspired in the
biological world where living organisms are built by cells and those
cells are built by information (DNA). Paul Spirakis explained us how
Network Constructions is a promising technique for modelling this idea
of "programmable matter". Broadly speaking, Network Constructions is
simply a collection of finite-automata that interact randomly like
molecules according to the rules of a common protocol.
The
last session on Thursday for me was the tutorial session by Louis-Marie
Traonouez by Plasma Lab, a statistical model checker (SMC). A SMC and
uses less resources than a model checker at the cost of losing
certainty. SMCs answers with a confidence level. Plasma Lab is SMC a
library written in Java that can be used in tools as UPPAAL. The
properties can be described in a form of bounded linear temporal logic
(like LTL but with bounds in the length of the paths).
The
last keynote talk of SOFSEM 2017 was on Friday and by Igor Walukiewicz.
The topic of the talk was automatic verification of recursive programs
with thread creation. Although this situation appears in programming
languages such as Java, Scala or Erlang it doesn't behave well in
automatic verification. For example, reachability is not decidable even
for pushdown systems where two threads are communicating over a 2-bit
shared variable. Igor Walukiewicz showed us some decidable setting by
relaxing the semantics of thread creation operation. The obtaining
result might not be very efficient but at least is computable.
Finally,
I want to end these notes on SOFSEM by acknowledging the excellent work
of the local organization at Limerick. It's true that SOFSEM 2017
didn't start very well in June, but all things considered everything
went smooth and fine in Limerick. Also, the organization always tried to
add something new to the conference (as those special talks about art
and computer science), which is always nice for the participants.
Next year SOFSEM will be held in Austria and my recommendation is to check it out!
