Using Machine Learning to support health system planning during the Covid-19 pandemic: a case study using data from São José dos Campos (Brazil)

Many efforts were made by the scientific community during the Covid-19 pandemic to understand the disease and better manage health systems' resources. Believing that city and population characteristics influence how the disease spreads and develops, we used Machine Learning techniques to provide insights to support decision-making in the city of São José dos Campos (SP), Brazil. Using a database with information from people who undergo the Covid-19 test in this city, we generate and evaluate predictive models related to severity, need for hospitalization and period of hospitalization. Additionally, we used the SHAP value for models' interpretation of the most decisive attributes influencing the predictions. We can conclude that patient age linked to symptoms such as saturation and respiratory distress and comorbidities such as cardiovascular disease and diabetes are the most important factors to consider when one wants to predict severity and need for hospitalization in this city. We also stress the need of a greater attention to the proper collection of this information from citizens who undergo the Covid-19 diagnosis test.

Open and Branching Behavioral Synthesis with Scenario Clauses

The Software Engineering community has identified behavioral specification as one of the main challenges to be addressed for the transference of formal verification techniques such as model checking. In particular, expressivity of the specification language is a key factor, especially when dealing with Open Systems and controllability of events and branching time behavior reasoning. In this work, we propose the Feather Weight Visual Scenarios (FVS) language as an appealing declarative and formal verification tool to specify and synthesize the expected behavior of systems. FVS can express linear and branching properties in closed and Open systems. The validity of our approach is proved by employing FVS in complex, complete, and industrial relevant case studies, showing the flexibility and expressive power of FVS, which constitute the crucial features that distinguish our approach.

The Design of a Verified Derivative-Based Parsing Tool for Regular Expressions

We describe the formalization of Brzozowski and Antimirov derivative based algorithms for regular expression parsing, in the dependently typed language Agda. The formalization produces a proof that either an input string matches a given regular expression or that no matching exists. A tool for regular expression based search in the style of the well known GNU grep has been developed with the certified algorithms. Practical experiments conducted with this tool are reported.

Set-Based Models for Cryptocurrency Software

Formal methods (FM) are mathematics-based software development methods aimed at producing ``code for a nuclear power reactor''. That is, due application of FM can produce bug-free, zero-defect, correct-by-construction, guaranteed, certified software. However, the software industry seldom use FM. One of the main reasons for such a situation is that there exists the perception (which might well be a fact) that FM increase software costs. On the other hand, FM can be partially applied thus producing high-quality software, although not necessarily bug-free. In this paper we outline some FM related techniques whose application the cryptocurrency community should take into consideration because they could bridge the gap between ``loose web code'' and ``code for a nuclear power reactor''. We include relevant case studies in the area of cryptocurrency.

Towards an Extrinsic Formalization of Featherweight Java in Agda

Featherweight Java is one of the most popular calculi which specify object-oriented programming features. It has been used as the basis for investigating novel language functionalities, as well as to specify and understand the formal properties of existing features for languages in this paradigm. However, when considering mechanized formalization, it is hard to find an implementation for languages with complex structures and binding mechanisms as Featherweight Java. In this paper we formalize Featherweight Java, implementing the static and dynamic semantics in Agda, and proving the main safety properties for this calculus.

Preface to the CLEI Electronic Journal Special Issue on Digital Healthcare

This special issue of the CLEI Electronic Journal (CLEIej) is dedicated to Digital Healthcare. It contains two accepted papers presenting research related to the COVID-19 pandemic in Latin America.

Chatbot as a Telehealth Intervention Strategy in the COVID-19 Pandemic

The COVID-19 pandemic and the need for social distancing have created a demand for new and innovative solutions in healthcare systems worldwide. One of the strategies that have been implemented are chatbots, which can be helpful in providing reliable health information and preventing people from seeking assistance in healthcare centers and being unnecessarily exposed to the virus. In this context, although a high number of chatbots have been implemented worldwide, little has been discussed about the process and challenges in developing and implementing this technology. This paper reports on an action research, which designed a novel chatbot as a prompt response to the COVID-19 pandemic. The chatbot is intended to be a first layer of interaction with the public, performing triage of patients and providing information about COVID-19 on a large scale and without human contact. Our contribution is twofold: (i) we reflected on the development process and discuss lessons learned and recommendations to support a multidisciplinary development and evolution process of the chatbot; and (ii) we identified some interactive and technological features that can be used as a reference framework for this kind of technology. These contributions can be useful to other researchers and multidisciplinary teams facing similar challenges.

Electronic Health Records (EHR) of the Emergency Service of the Hospital de Clínicas: Case Study

The automation of the management in the Emergency Service of the Hospital de Clinicas of the Universidad Nacional de Asuncion is a problem addressed in this work since the care of the patient in critical condition must be accurate, appropiate and efficient. The development of a management automation tool will generate benefits for both the patient and the hospital's target staff. With the automatization of the processes, which are still done manually, it will be possible to achieve: (a) more time to devote to a better patient care, (b) doctors will be able to spend part of their time to analyze the statistics and information, which can be generated through the application to carry out investigations in the area of emergency care, and (c) as well as to optimize the resources of both the staff and the logistics used in the Hospital. To achieve the proposed objective, in this work a complete and Electronic Health Records System management based on international health standards has been developed, as well as good practices in the care processes in an area as sensitive as the Emergency Service. After more than 100 years of history of the Hospital, for the first time it is intended to automate processes and generate online information quickly and efficiently from this modern tool optimizing patient care in the emergency area.

Market basket analysis with association rules in the retail sector using Orange. Case Study: Appliances Sales Company

This research is conducted to analyze the shopping basket by using association rules in the retail area, more specifically in a home goods sales company such as appliances, computer items, furniture, and sporting goods, among others. With the rise of globalization and the advancement of technology, retail companies are constantly struggling to maintain and raise their profits, as well ordering the products and services that the customer wants to obtain. In this sense, they need a new approach to identify different objectives in order to be more competitive and successful, looking for new decision-making strategies. To achieve this goal, and to obtain clear and efficient strategies, by providing large amounts of data collected in business transactions, the need arises to intelligently analyze such data in order to extract useful knowledge that will support decision-making and, an understanding of the association patterns that occur in sales-customer behavior. Predicting which product will make the most profit, products that are sold together, this type of information is of great value for storing products in inventory. Knowing when a product is out of fashion can support inventory management effectively. In this sense, this work presents the rules of association of products obtained by analyzing the data with the FPGrowth algorithm using the Orange tool.

Performance Analysis of Deep Learning Methods for Protein Contact Prediction in CASP13

Protein structure prediction is one of the most important problems in Computational Biology; and consists of determining the 3D structure of a protein given its amino acid sequence. A key component that has allowed considerable improvements in recent decades is the prediction of contacts in a protein, since it provides fundamental information about its three-dimensional structure. In the 13th edition of the CASP (Critical Assessment of protein Structure Prediction), a notable progress has been evidenced for both problems with the use of deep learning algorithms. For the contact prediction category, the best methods in CASP13 achieved an average precision of 70%. In the present work, the performance of these methods is analyzed using a larger data set, with 483 proteins from four families according to the structural classification of the SCOP database (Structural Classification of Proteins). The selected methods were evaluated using the CASP metrics, and their results indicate an average contact prediction precision greater than 90%. SPOT-Contact was the method with the best overall performance, and one of the methods with the best performance for each SCOP class. The set of proteins used for the experiments and the implementations made for the analysis are publicly available.