Abstract
Formal verification has become increasingly crucial in ensuring the accurate and secure functioning of modern software systems. Given a specification of the desired behaviour, i.e. a contract, a program is considered to be correct when all possible executions guarantee the specification. Should the software fail to behave as expected, then a bug is present. Most existing research assumes that the bug is present in the implementation, but it is also often the case that the specified expectations are incorrect, meaning that it is the specification that must be repaired. Research and tools for providing alternative specifications that fix details missing during contract definition, considering that the implementation is correct, are scarce. This paper presents a preliminary tool, focused on Dafny programs, for automatic specification repair in contract programming. Given a Dafny program that fails to verify, the tool suggests corrections that repair the specification. Our approach is inspired by a technique previously proposed for another contract programming language and relies on Daikon for dynamic invariant inference. Although the tool is focused on Dafny, it makes use of specification repair techniques that are generally applicable to programming languages that support contracts. Such a tool can be valuable in various scenarios, such as when programmers have a reference implementation and need to analyse their contract options, or in educational contexts, where it can provide students with hints to correct their contracts. The results of the evaluation show that the approach is feasible in Dafny and that the overall process has reasonable performance but that there are stages of the process that need further improvements.

Abstract
In the last few years we have been seeing a drastic change in the way software is developed. Large-scale software projects are being assembled by a flexible composition of many (small) components possibly written in different programming languages and deployed anywhere in the cloud - the so-called microservices-based applications. The dramatic growth in popularity of microservices-based applications has pushed several companies to apply major refactorings to their software systems. However, this is a challenging task that may take several months or even years. We propose a methodology to automatically evolve monolithic web applications that use object-relational mapping into microservices-based ones. Our methodology receives the source code and a microservices proposal and refactors the original code to create each microservice. Our methodology creates an API for each method call to classes that are in other services. The database entities are also refactored to be included in the corresponding service. The evaluation performed in 120 applications shows that our tool can successfully refactor about 72% of them. The execution of the unit tests in both versions of the applications yield exactly the same results.

Abstract
Although remote work was already possible and used in some contexts, the COVID-19 pandemic made it normal and, in some situations, even mandatory. This was the case in Portugal and in particular in its software industry. Given this abrupt change in how we work, it became pressing to investigate the impacts of this profound change to remote work, so that we can cope with the potential negative consequences (professional, personal, etc.). Thus, the goal of this work is to study the impact of the referred change to remote work, due to the COVID-19 pandemic, on software professionals in Portugal. To achieve this goal, a survey was prepared and distributed via email, LinkedIn, and Instagram. In total, 176 valid answers were collected from software professionals working in Portugal from 38 different companies. After the performed statistical analysis on the targeted population and focusing on the 10 elaborated research questions, two major findings can be concluded with certainty: (i) having worked in a remote regime before the pandemic period has a strong relationship with a higher frequency of use of teleconference tools after this period, and (ii) participants who do not feel safe about coming back to a fully on-site regime are more likely to prefer a fully remote regime than the ones who feel safe, while the latter group is more likely to prefer a hybrid regime. © 2023 CIbSE 2023 - XXVI Ibero-American Conference on Software Engineering. All rights reserved.

Abstract

Abstract
The architectural style of microservices has received much attention from both business and academia and converting a monolithic application into a microservice-based one has become a regular practice. However, companies struggle with migrating their existing monolithic applications to microservices and software engineers frequently face challenges due to a lack of awareness of alternative migration methodologies, making the migration process even harder. In this paper, we present a framework to help software engineers during the migration process by addressing gaps in understanding various migration tools and approaches, allowing for easy comparison between multiple options. Our tool combines multiple existing approaches into one platform, allowing a comprehensive visualization of migration proposals and comparing different options offered by already existing approaches.

Abstract
Continuous Integration and Continuous Deployment (CI/CD) pipelines play a vital role in the DevOps process, enabling developers to automate and enhance software delivery. However, the existence of multiple technologies, such as GitHub Actions, GitLab CI/CD, or Jenkins, poses challenges due to their lack of interoperability and the use of different programming languages for pipeline construction. To address these challenges and improve the CI/CD process, our objective is to develop a block-based language specifically designed for representing CI/CD pipelines. With our language, we intend to empower users to more easily create correct pipelines. Through an interactive and user-friendly process, our approach guides users in constructing pipelines, ensuring accuracy and reducing errors. Additionally, our language will facilitate seamless transitions between different pipeline technologies, providing users with flexibility and ease of adoption.