The FM’19 – 3rd World Congress on Formal Methods, an event that gathers the worldwide computer experts, took place in Porto between 7 and 11 October. Around 600 experts from more than 40 different nationalities attended this international congress, known as the largest international congress on the Formal Methods area.
FM’19, which aims at bringing together researchers, academics and technology industry professionals operating in the computer science field, in particular those that investigate the Formal Methods topic as a way to promote the quality and reliability in an increasingly technological and socially relevant sector, had over 30 side events, including nine conferences, two festschrifts, 16 workshops, five tutorials and other events such as Industry Day and Doctoral Symposium.
To José Nuno Oliveira, president of the organising committee, senior researcher at INESC TEC and Professor at the University of Minho, “the variety and quantity of side events of FM’19 allowed us to establish synergies between several fields of knowledge in the Computer Science area, thus stimulating the intersection of scientific outcomes and the advancement of this important science as we know today”.
FM’19, which took place in three locations in the city of Porto – the Alfândega Porto’s building, the World of Discoveries Museum and the Vincci Porto Hotel, reached a record of 381 scientific articles submitted and presented by researchers, academics and industry professionals in this field of knowledge.
FM’19 was financially supported by companies such as AWS, Google, SONY, Springer, Semmle, ASML, Oracle, Efacec and other national and international companies. Still related to the technological industry, it is important to highlight the presence of renowned institutions, such as Apple, Airbus, Booking.com, ESA, Fraunhofer, Microsoft, MathWorks, NASA, Samsung, VERIMAG, among others.
It should also be noted that the organisation of FM’19 was under the responsibility of INESC TEC, alongside the University of Minho and the Formal Methods Europe association, which promotes the organisation of this congress every 10 years.
Turing Award was present at FM’19
Tony Hoare, winner of a Turing Award in 1980, a distinction in the Computer Science field that is generally recognised as the Computing Nobel Prize, was present at FM’19. The lecture of this 85-year-old expert took place on 8 October within the scope of the UTP 2019 – 7th International Symposium on Unifying Theories of Programming conference.
“The presence of Tony Hoare, one of the living legends of Programming Science, was definitely one of the highlights of the congress, coinciding with the 50th anniversary of one of his most important papers,” adds José Nuno Oliveira. The scientific paper “An Axiomatic Basis for Computer Programming” was published on October of 1969 in the Communications of the ACM and to this day remains one of the most quoted paper in this area.
The importance of Formal Methods
Formal methods “are programming techniques that achieve high levels of quality and reliability through the mathematical treatment of problems that can be addressed by software. All military, security, energy, health, education systems, all back offices and company’s operating systems — well, all the systems in which our civilisation is based on — rely on sophisticated software that is continuously being developed so that they can operate and serve us. In safety critical issues, programming errors can have devastating consequences. This is where Formal Methods become very important tools. This is one of the research lines of INESC TEC’s High-Assurance Software Laboratory (HASLab), which has a vast experience in this area, applying Formal Methods in areas such as security, human-computer interaction, model checking, program calculation and verification, and more recently, quantum programming”, explains José Nuno Oliveira.
INESC TEC’s participation highlighted
Besides the organising team, there were INESC TEC researchers involved in the presentation of scientific papers in several events of the world congress, namely:
- An Adequate While-Language for Hybrid Computation
Sergey Goncharov and Renato Neves
- A dynamic logic for QASM programs (Short paper)
- Behavioural and Abstractor Specifications for Dynamic Logic with Binders and Silent Transitions
Rolf Hennicker, Alexander Knapp and Alexandre Madeira
- On the construction of multi-valued concurrent dynamic logic (Short paper)
- Logic, Algebra, and Geometry at the Foundation of Computer Science (Tutorial)
Tony Hoare, Alexandra Mendes and João Ferreira
- Panel Discussion on Teaching Program Development
Catherine Dubois, Thiago Mendonça Ferreira Ramos, María del Mar Gallardo, Kristin Rozier and Alexandra Mendes
- Open and Interactive Learning Resources for Algorithmic Problem Solving
João Ferreira and Alexandra Mendes
- Model-Based Testing of Post-WIMP Interactions Using Petri-nets
Alexandre Canny, David Navarre, José Creissac Campos and Philippe Palanque
- Examples of the application of formal methods to interactive systems (Invited Talk)
- Simulation under arbitrary temporal logic constraints
Julien Brunel, David Chemouil, Alcino Cunha and Nuno Macedo
- GOSPEL – Providing OCaml with a Formal Specification Language
Arthur Charguéraud, Jean-Christophe Filliâtre, Cláudio Lourenço and Mário Pereira
In addition to this, Alcino Cunha and Nuno Macedo were involved in the organisation of the ALLOY tutorial, Luís Soares Barbosa was responsible for the organisation of the DALI workshop and José Creissac Campos was in the organisation of the FMIS workshop.
During the week, nine awards were given in different categories and events, including the Peter Lucas Award, the FME Fellowship Award and the Best Tool Paper Award given at FM 2019; the Radhia Cousot Young Researcher Award was given to two researchers at SAS 2019; the Best Paper Award and The Test of Time Award were delivered at RV 2019; the Best Presentation Award was given at the Doctoral Symposium, and the Best Paper Award was given at LOPSTR 2019.
The researchers mentioned in this news piece are associated with INESC TEC, UMinho, University of Beira Interior and University of Aveiro.