DEI Talks | Formal Verification of Distributed Systems by Julien Brunel and David Chemouil

Julien Brunel and David Chemouil are senior researchers at ONERA, in Toulouse, specialized in formal specification and verification. Together with Nuno Macedo and Alcino Cunha (INESC TEC) they designed the 6th version (dubbed Electrum until recently) of the Alloy language and tool (originally proposed by the MIT). In recent years, Julien Brunel and David Chemouil have also been studying the verification of distributed algorithms. A recent highlight is the first mechanical proof of correctness of the distributed maintenance algorithm of the Chord peer-to-peer protocol, as well as formal techniques for the complete, semi-automatic verification of infinite-state systems, such as distributed algorithms.

Join us on the 8th April, at 14:30, in room I-105 of FEUP, for the presentation of this work.

Abstract:

The verification of distributed systems is challenging because these systems combine a rich structure, a high number of elements and a non-trivial temporal evolution. A trade-off between automation and completeness of the verification has to be made. In particular, one can use theorem provers, which offer complete confidence but tend to require considerable expertise and effort. Another option is to use model checkers, which offer complete automation, but cannot handle complex data structures and configurations.

In this talk, they will present recent work on verification techniques for distributed systems that are automatic and “as complete as possible”, or complete and “as automatic as possible”. They will illustrate their work with the analysis of Chord, a scalable distributed hash table.

INFORMATICS.OnBoard, the Informatics Engineering * Interpares Mentoring Program, promoted last April 2nd another social event between L.EIC 1st year students and their mentors.

The group went out to discover the “Little Portuguese Tibet” through the Brandas de Sistelo Trail (PR14 Walk). In this scenery of true rural beauty, where the fabulous terraces stand out in the landscape, students and teachers were able to socialize informally, in collaborative dynamics that promote mutual help, integration, friendship and well-being.

This was the second activity of the 2021/2022 edition. All the others can be seen at Informatics On Board

* Interpares Mentoring Program

 The Faculty of Engineering of the University of Porto has an INTERPARES MENTORING program in operation, aimed at students entering for the first time in this institution of Higher Education (mentees), both national and international, with the objective of supporting them in this new phase of their academic path. This program of social and academic integration is carried out by students (mentors) already attending the different courses in more advanced years, and coordinated by a team of teachers, being adapted to each course according to its characteristics. This program is totally voluntary for both mentors and mentees. This initiative is currently integrated in the U. Porto Mentoring Program.

DEI Talks | JUMPING FINITE AUTOMATA by Prof. Alexander Meduna

Prof. Alexander Meduna (born 1957 in Olomouc, Czech Republic ) is a theoretical computer scientist and expert on compiler design, formal languages and automata. He is a professor of Computer Science at the Brno University of Technology. Formerly, he taught theoretical computer science at various European and American universities, including the University of Missouri, where he spent a decade teaching advanced topics of formal language theory. He wrote over ninety papers related to theoretical computer science.

Join us on the 7th April, at 14:30, in room I-105 of FEUP, for the presentation of JUMPING FINITE AUTOMATA

Abstract:

This talk proposes a new investigation area in automata theory — jumping finite automata. These automata work like classical finite automata except that they read input words discontinuously — that is, after reading a symbol, they can jump over some symbols within the words and continue their computation from there. The talk gives several results concerning jumping finite automata in terms of commonly investigated areas of automata theory, such as closure properties. Most importantly, it achieves several results that demonstrate differences between jumping finite automata and classical finite automata. In its conclusion, the talk  formulates several open problems and suggests future investigation areas.

His latest book is Handbook of Mathematical Models for Languages and Computation

Meduna, Alexander; Tomko, Martin, Horacek, Petr (2019)

The Institution of Engineering and Technology, Stevenage, UK, ISBN: 978-1-78561-660-0

https://www.amazon.ae/Handbook-Mathematical-Models-Languages-Computation/dp/1785616595

His previous books include

  • Meduna, Alexander (2000). Automata and Languages: Theory and Applications. Springer Science & Business Media. ISBN 9781852330743.
  • Meduna, Alexander (2007). Elements of Compiler Design. CRC Press. ISBN 9781420063233.
  • Meduna, Alexander (2014). Formal Languages and Computation: Models and Their Applications. CRC Press. ISBN 9781466513457.
  • Meduna, Alexander; Švec, Martin (2005). Grammars with Context Conditions and Their Applications. John Wiley & Sons. ISBN 9780471736554.
  • Meduna, Alexander; Techet, Jiří (2010). Scattered Context Grammars and Their Applications. WIT Press. ISBN 9781845644260.
  • Meduna, Alexander; Zemek, Petr (2014). Regulated Grammars and Automata. Springer. ISBN 9781493903696.
  • Meduna, Alexander; Soukup, Ondřej (2017). Modern Language Models and Computation: Theory with Applications. Springer. ISBN 9783319630991.

PhD Defense in Informatics Engineering: ”Increasing the Dependability of Internet-of-Things Systems in the context of End-User Development Environments”

Candidate:
João Pedro Matos Teixeira Dias

Date, Time e Place
1st of April, 09:00, remotely with streaming at: https://www.youtube.com/channel/UCvsg2ymeaHLRLbsGt67JmKw

President of the Jury
PhD Rui Filipe Lima Maranhão de Abreu, Full Professor at Faculdade de Engenharia da Universidade do Porto

Members
PhD Dariusz Mrozek, Associate Professor at the Department of Applied Informatics at Silesian University of Technology, Poland;
PhD Pedro Nicolau Faria da Fonseca, Assistant Professor at the Department of Electronics, Telecommunications and Informatics of Universidade de Aveiro;
PhD André Monteiro de Oliveira Restivo, Assistant Professor at the Department of Informatics Engineering of Universidade do Porto;
PhD Hugo José Sereno Lopes Ferreira, Assistant Professor at the Department of Informatics Engineering of Universidade do Porto (Supervisor).

Abstract:

The ubiquitousness of computing, known as Internet-of-Things (IoT), has reshaped the way people interact with the physical world. However, the scale, distribution — both logical and geographical –, density, heterogeneity, interdependence, and {quality-of-service} requirements of these systems make them complex, posing several challenges from both operational and development viewpoints.

While there is a consensus that the widely used software engineering practices are inadequate for IoT development, they remain the go-to solutions for most practitioners. This aspect has severely compromised their dependability, centralizing most of the computation of these (soft) real-time systems in cloud infrastructure. Likewise, as these systems scale in terms of devices and applications, it outreaches existing technical resources to manage and operate them, becoming of paramount importance, making them as most self-managed as possible while empowering the ability of system operators (including end-users) to configure and understand them — mainly using solutions that do not require high technical expertise, viz. low-code development solutions — including the configuration of fail-safe measures.

This dissertation’s primary focus is to research how to improve the current status quo on the dependability of IoT. However, this is a manifold endeavor: (1) what are the best practices for developing IoT dependably, and what is their scientific soundness, (2) do the current solutions give the fundamental building blocks that allow to design and construct dependable systems, and, if not, what contributions are needed to overcome the existing limitations, and, lastly, (3) giving that these systems are operated by humans with limited technical expertise, it is required that their users can use and configure them without compromising their correct operation. As we set ourselves to tackle these challenges, we claim that:

It is possible to enrich IoT-focused end-user development environments in such a way that the resulting systems have a higher dependability degree, with the lowest impact on the know-how of the (end-)users.

As preliminary research, to understand what end-users want to automate and how they wish to perform such automations, a study was carried to collect automation scenarios. These scenarios showcased the complexity of the automations that some end-users want to perform and the interdependencies between different information sources, devices, and persons. It also supported the view that some of the appliances that end-users want to automate can have nefarious effects if a malfunction happens or a misconfiguration is performed.

We followed extensive literature research and experimental process to mine a set of patterns that can be used to improve IoT systems by making them more dependable, documenting them as patlets, which summarily describe solutions that address some particular problem within a specific context. We further studied a subset of these patterns as a self-healing pattern language that contemplates the use of more than one pattern in tandem to address systems’ operational concerns autonomically.

Adopting these patterns depends on supporting foundations, which include architectural and functional aspects of the target systems. A key aspect is that most of the current solutions do not provide any features to readjust their intrinsic behaviors during runtime — with the software that runs on edge devices being mostly set on stone, delegating all the computational needs to cloud-based services. The research on fog and edge computing attempt to mitigate this by leveraging computational resources across architectural tiers, making the resulting systems more dependable and improving their scalability. Taking on these foundations, we explored and asserted the feasibility of using serverless functions in the IoT context, optimizing the choice of execution contexts according to a priori preferences, constraints, and latencies.

To understand how these paradigms can be leveraged in widely used solutions, we select the open-source Node-RED solution as the experimental base, given its popularity. It provides a visual programming interface that increases its target user base across different expertise levels. Like other available solutions, Node-RED does not provide any feature that allows it to orchestrate tasks across devices or deal with system parts’ failures, limiting the dependability of systems built with it. Nonetheless, given its open-source and extensible nature, we proceed to address some of its limitations. We proceed to evaluate empirically, both in virtual and physical setups, the feasibility of using Node-RED as an orchestrator, where computational tasks are allocated to the available resources, and failures are mitigated by re-orchestrating as devices fail and recover. We also implemented a set of extensions for Node-RED that allows one to enrich the existing programs (i.e., flows) with self-healing capabilities — allowing the detection errors of different parts during runtime, and readjust its behavior to keep delivering correct service by recovering to normal operation, or, at least, maintain its operation within acceptable Quality-of-Service levels.

As IoT users have different expertise levels, we also attempt to improve the interaction with these systems in a way that the users can understand what the configured automations are (viz. inspection), how it is behaving (viz. observability and feedback), and increase their capability to know what was the possible cause behind certain events (viz. causality). In the first study, we extended the visual notations and functionalities of Node-RED to improve the development process using it. We proceed to empirically evaluate the performance of our solution against a non-modified version of Node-RED, observing statistically significant improvements in the users’ ability to evolve existing IoT deploys. Lastly, we explored the use of voice assistants as an alternative way of configuring, understanding, and interacting with IoT-enriched environments, with a particular focus on the ability of a user to understand the cause behind some events. We assert the feasibility of our solution by covering all the different automation possibilities that Node-RED supports, with a considerable extension of the interaction possibilities due to multi-message dialogs support. We proceeded to empirically validate the feasibility of users using the voice assistant to complete different tasks, and all the users were able to finish the tasks. While some valid sentences were incorrectly recognized, forcing the user to repeat their intent, participants expressed a preference for voice interfaces over visual ones in terms of subjective perception.

These contributions materialize into a core set of building blocks that, in assemble, can be used to improve the dependability of IoT systems while leveraging abstractions that do not hinder the (end-)user capability to configure, use, and evolve them. The experimental counterparts of the contributions provide empirical supporting evidence for the plausibility of the hypothesis.

Talk | “Interactive Music Analysis using the DFT and Pitch-Class Distributions extracted from MIDI files” by Fabian C. Moss

Fabien C. Moss is a Research Fellow in Cultural Analytics at University of Amsterdam (UvA). Working with large symbolic datasets of musical scores and harmonic annotations, he is primarily interested in Computational Music Analysis, Music Theory, Music Cognition, and their mutual relationship. His research is inherently interdisciplinary and aims to bridge the humanities and the sciences by drawing on methods and concepts from the Musicology and Music Theory, Mathematics, Music Information Retrieval, Data Science and Machine Learning, Music Psychology and Cognition, and the Digital Humanities.

Join us on the 4th of April, at 14:30, in room B015 of FEUP, for the presentation of “Interactive Music Analysis using the DFT and Pitch-Class Distributions extracted from MIDI files

By the author:

“The discrete Fourier transform (DFT) is a cornerstone of digital signal processing and commonly used to extract periodicities in time-continuous signals.

In recent years, however, mathematical music theorists have begun to explore DFT’s potential when applied not to the time but to the pitch-class domain, where the periodicities are given by equal divisions of the octave [1-3]. Earlier this year, we introduced wavescapes [4], a visualization method of hierarchical pitch-class relations in pieces of music.

Building on this work, we are currently developing midiVERTO [5], an interactive web app to analyze MIDI files using the DFT, that allows users to create wavescapes and inspect the dynamics of pitch-class distributions at several hierarchical levels. In my presentation, I will briefly introduce the underlying theoretical work followed by a tutorial on how to use the app for music analysis.

[1] Amiot (2016). Music Through Fourier Space: Discrete Fourier Transform in Music Theory. Springer.

[2] Noll (2019). Insiders’ Choice: Studying Pitch Class Sets Through Their Discrete Fourier Transformations. InMathematics and Computation in Music (pp. 371–378). Springer. https://doi.org/10.1007/978-3-030-21392-3_32

[3] Tymoczko & Yust (2019). Fourier Phase and Pitch-Class Sum. In Mathematics and Computation in Music (pp. 46–58). Springer. https://doi.org/10.1007/978-3-030-21392-3_4

[4] Viaccoz, C., Harasim, D., Moss, F. C., & Rohrmeier, M. (2022). Wavescapes: A visual hierarchical analysis of tonality using the discrete Fourier transform. Musicae Scientiaehttps://doi.org/10.1177/10298649211034906

[5] Harasim, D., Affatato, G., & Moss, F. C. (2022). midiVERTO: A Web Application to Visualize Tonality in Real Time. arXiv:2203.13158 [cs]http://arxiv.org/abs/2203.13158

Tenders for the recruitment of 2 Assistant Professors for the disciplinary area of Informatics Engineering

Deadline for applications 28th of April 2022

Public Notice 279/2022

Professor José Manuel Pereira Dias de Castro Lopes, Full Professor of the Faculty of Medicine of the University of Porto and Vice-Rector of the University of Porto:
Following my Order issued on February 25th, 2022, by delegated power under the Ordinance no. 8378/2021 published in the Official Gazette, 2nd series, no. 164 of 24 August this call for applications is published for one position of Assistant Professor in the area of Informatics Engineering of the Faculty of Engineering of this University. The application procedure will remain in force for a period of 30 (thirty) business days as from the date immediately following the publication of this Notice in the Official Gazette. Edital EN

Public Notice 280/2022

Professor José Manuel Pereira Dias de Castro Lopes, Full Professor of the Faculty of Medicine of the University of Porto and Vice-Rector of the University of Porto:
Following my Order issued on February 25th, 2022, by delegated power under the Ordinance no. 8378/2021 published in the Official Gazette, 2nd series, no. 164 of 24 August this call for applications is published for one position of Assistant Professor in the area of Informatics Engineering of the Faculty of Engineering of this University. The application procedure will remain in force for a period of 30 (thirty) business days as from the date immediately following the publication of this Notice in the Official Gazette. Edital EN

PhD Defense in Digital Media: ”Instagram Photography: Toward the profiling of photography sharing modes of practice”

Candidate:
Cláudio António Moreira Alves do Carmo Reis

Date, Time e Place
29 de março, às 10h00, na Sala de Atos da Faculdade de Engenharia e por videoconferência.

Streaming: https://www.youtube.com/channel/UCvsg2ymeaHLRLbsGt67JmKw

President of the Jury
Doutor António Fernando Vasconcelos Cunha Castro Coelho, Professor Associado c/ Agregação da FEUP

Members
Doutora Luísa Maria Lopes Ribas, Professora Auxiliar da Faculdade de Belas Artes da Universidade de Lisboa;
Doutora Sandra Vieira Jürgens, Professora Auxiliar Convidada do Departamento de História da arte da Faculdade de Ciências Sociais e Humanas da Universidade Nova de Lisboa;
Doutor João Pedro Ferreira Dias Leal, Professor Adjunto da Escola Superior de Media Artes e Design do Instituto Politécnico do Porto;
Doutor Pedro Leão Ramos Ferreira Neto, Professor Auxiliar da Faculdade de Arquitetura da Universidade do Porto;
Doutor Gilberto Bernardes de Almeida, Professor Auxiliar do Departamento de Engenharia Informática da Faculdade de Engenharia da Universidade do Porto;
Doutor José Manuel da Silva Fernandes de Carvalho Carneiro, Professor Auxiliar do Departamento de Design da Faculdade de Belas Artes da Universidade do Porto (Orientador).

‹Programming› 2022, Porto + Online

The International Conference on the Art, Science, and Engineering of Programming is a new conference focused on programming topics including the experience of programming. It was named ‹Programming› for short. ‹Programming› seeks for papers that advance knowledge of programming on any relevant topic, including programming practice and experience.
After Brussels, Nice, Genova, Porto, Cambridge, this sixth edition will follow a dual format, taking place in two moments, two venues, to offer two different kinds of experience:

First in Porto, Mon 21 – Fri 25 March, 2022, a charming city that will be happy to be able to embrace the participants, as soon as they arrive;
Later in an online venue, Mon 11 – Thu 14 April, 2022, 4 days, 2.5 hours/day, in different timezones, to welcome all around the world.

Ademar Aguiar, Associate Professor @DEI/FEUP, is the General Chair for this edition and tells us that the week ahead will be full of interesting sessions, with 2 keynotes, 15 talks, 6 demos, 3 workshops, 1 tutorial.
In addition, an Open Space track will welcome and host last minute ideas and interests on leading sessions among all participants.

The Social Program includes several social events, providing a mashup of Porto’s attractions, from historical to cultural, gastronomic and social, including local academy and industry. All of this to promote informal and playful conversations, to make sure that the experience will be unique and memorable.

Back to the future is the motto for 2022!

For + info and registration: https://2022.programming-conference.org/

CreativityTalks | Prof. António Sampaio da Nóvoa will be our next guest

There are many “futurisms” that suggest an education without schools, based on the immense possibilities of technologies and artificial intelligence. These “futurisms” gained strength with the pandemic and the different forms of isolation to which we have been subjected. But education does not take place in “confinement”, it always requires a relationship, an encounter, working together. This is not the time to announce the “death of school”, but rather to invent it anew.

“Inventing the School anew” will be the topic of the 6th Creativity Talk, presented by Professor *António Sampaio da Nóvoa, on March 17, at 18:00, at the FEUP’s Anfiteatro Nobre (B032).

The session will be moderated by Amélia Lopes, Full Professor and President of the Scientific Council of the Faculty of Psychology and Education Sciences of the University of Porto.

The participation in the lecture requires a (free) registration at Eventbrite (places available to the capacity of the room by order of registration).

If you cannot attend in person, you can attend remotely through the following address: https://youtu.be/V2I0h0EQBO0

*Bio

António Sampaio da Nóvoa is a Full Professor at the University of Lisbon. He holds a PhD in History from the University of Paris IV-Sorbonne and a PhD in Education Sciences from the University of Geneva. He was Rector of the University of Lisbon between 2006 and 2013. He was Portugal’s Ambassador to UNESCO between 2018 and 2021.

DEI Talks | The Digital Score – “What’s really going on {in} here?” by Prof. Craig Vear

Prof Craig Vear is a Research Professor at De Montfort University where he is also a director of the Creative AI and Robotics Lab in the Institute of Creative Technologies. His research is naturally hybrid as he draws together the fields of music, digital performance, creative technologies, artificial intelligence, creativity, gaming, mixed reality and robotics. He has been engaged in practice-based research with emerging technologies for nearly three decades, and was editor for The Routledge International Handbook of Practice-Based Research, published in 2022. His recent monograph The Digital Score: creativity, musicianship and innovation, was published by Routledge in 2019, and he is Series Editor of Springer’s Cultural Computing Series. In 2021 he was awarded a €2Million ERC Consolidator Grant to continue to develop his Digital Score research – digiscore.dmu.ac.uk 

Join us on the 24th February, at 14:30, in room B024 of FEUP, for the presentation and discussion of this project – Investigating Technological Transformation of the Music Score (DigiScore).

The opening section will position the digital score amongst a broader understanding of the function and purpose of all music scores: that of a communications interface between musicians. After defining that which signals a digital score as a different proposition, he will outline the research aims and objectives of the DigiScore project. Will position this research among the core principles of flow, phenomenology, embodiment, and media affect, and outline the focus of the research as seeking meaning-making from inside the creative acts of digital score musicking (Small 1989). The final section will outline some of the current new insights, and present key questions that he would wish to discuss with those present in the room as way of allowing their voice into the development of this researchers and expanding the community of research in this area.