Showing 1–36 of 36 results for author: Sousa, M

Eery Space: Facilitating Virtual Meetings Through Remote Proxemics

Authors: Maurício Sousa, Daniel Mendes, Alfredo Ferreira, João Madeiras Pereira, Joaquim Jorge

Abstract: Virtual meetings have become increasingly common with modern video-conference and collaborative software. While they allow obvious savings in time and resources, current technologies add unproductive layers of protocol to the flow of communication between participants, rendering the interactions far from seamless. In this work we introduce Remote Proxemics, an extension of proxemics aimed at bring… ▽ More Virtual meetings have become increasingly common with modern video-conference and collaborative software. While they allow obvious savings in time and resources, current technologies add unproductive layers of protocol to the flow of communication between participants, rendering the interactions far from seamless. In this work we introduce Remote Proxemics, an extension of proxemics aimed at bringing the syntax of co-located proximal interactions to virtual meetings. We propose Eery Space, a shared virtual locus that results from merging multiple remote areas, where meeting participants' are located side-by-side as if they shared the same physical location. Eery Space promotes collaborative content creation and seamless mediation of communication channels based on virtual proximity. Results from user evaluation suggest that our approach is effective at enhancing mutual awareness between participants and sufficient to initiate proximal exchanges regardless of their geolocation, while promoting smooth interactions between local and remote people alike. These results happen even in the absence of visual avatars and other social devices such as eye contact, which are largely the focus of previous approaches. △ Less

Submitted 1 June, 2024; originally announced June 2024.

Comments: 19 pages, 7 figures

Journal ref: INTERACT 2015. Lecture Notes in Computer Science(), vol 9298. Springer, Cham

4Doodle: Two-handed Gestures for Immersive Sketching of Architectural Models

Authors: Fernando Fonseca, Maurício Sousa, Daniel Mendes, Alfredo Ferreira, Joaquim Jorge

Abstract: Three-dimensional immersive sketching for content creation and modeling has been studied for some time. However, research in this domain mainly focused on CAVE-like scenarios. These setups can be expensive and offer a narrow interaction space. Building more affordable setups using head-mounted displays is possible, allowing greater immersion and a larger space for user physical movements. This pap… ▽ More Three-dimensional immersive sketching for content creation and modeling has been studied for some time. However, research in this domain mainly focused on CAVE-like scenarios. These setups can be expensive and offer a narrow interaction space. Building more affordable setups using head-mounted displays is possible, allowing greater immersion and a larger space for user physical movements. This paper presents a fully immersive environment using bi-manual gestures to sketch and create content freely in the virtual world. This approach can be applied to many scenarios, allowing people to express their ideas or review existing designs. To cope with known motor difficulties and inaccuracy of freehand 3D sketching, we explore proxy geometry and a laser-like metaphor to draw content directly from models and create content surfaces. Our current prototype offers 24 cubic meters for movement, limited by the room size. It features infinite virtual drawing space through pan and scale techniques and is larger than the typical 6-sided cave at a fraction of the cost. In a preliminary study conducted with architects and engineers, our system showed a clear promise as a tool for sketching and 3D content creation in virtual reality with a great emphasis on bi-manual gestures. △ Less

Submitted 27 June, 2024; v1 submitted 29 May, 2024; originally announced May 2024.

Comments: 9 pages; 15 Figures

MSC Class: H.5.2; I.3.4; I.3.7 ACM Class: H.5.2; I.3.4; I.3.7

GloSIS: The Global Soil Information System Web Ontology

Authors: Raul Palma, Bogusz Janiak, Luís Moreira de Sousa, Kathi Schleidt, Tomáš Řezník, Fenny van Egmond, Johan Leenaars, Dimitrios Moshou, Abdul Mouazen, Peter Wilson, David Medyckyj-Scott, Alistair Ritchie, Yusuf Yigini, Ronald Vargas

Abstract: Established in 2012 by members of the Food and Agriculture Organisation (FAO), the Global Soil Partnership (GSP) is a global network of stakeholders promoting sound land and soil management practices towards a sustainable world food system. However, soil survey largely remains a local or regional activity, bound to heterogeneous methods and conventions. Recognising the relevance of global and tran… ▽ More Established in 2012 by members of the Food and Agriculture Organisation (FAO), the Global Soil Partnership (GSP) is a global network of stakeholders promoting sound land and soil management practices towards a sustainable world food system. However, soil survey largely remains a local or regional activity, bound to heterogeneous methods and conventions. Recognising the relevance of global and trans-national policies towards sustainable land management practices, the GSP elected data harmonisation and exchange as one of its key lines of action. Building upon international standards and previous work towards a global soil data ontology, an improved domain model was eventually developed within the GSP [54], the basis for a Global Soil Information System (GloSIS). This work also identified the Semantic Web as a possible avenue to operationalise the domain model. This article presents the GloSIS web ontology, an implementation of the GloSIS domain model with the Web Ontology Language (OWL). Thoroughly employing a host of Semantic Web standards (SOSA, SKOS, GeoSPARQL, QUDT), GloSIS lays out not only a soil data ontology but also an extensive set of ready-to-use code-lists for soil description and physio-chemical analysis. Various examples are provided on the provision and use of GloSIS-compliant linked data, showcasing the contribution of this ontology to the discovery, exploration, integration and access of soil data. △ Less

Submitted 25 March, 2024; originally announced March 2024.

Highly Reproducible and CMOS-compatible VO2-based Oscillators for Brain-inspired Computing

Authors: Olivier Maher, Roy Bernini, Nele Harnack, Bernd Gotsmann, Marilyne Sousa, Valeria Bragaglia, Siegfried Karg

Abstract: With remarkable electrical and optical switching properties induced at low power and near room temperature (68C), vanadium dioxide (VO2) has sparked rising interest in unconventional computing among the phase-change materials research community. The scalability and the potential to compute beyond the von Neumann model make VO2 especially appealing for implementation in oscillating neural networks… ▽ More With remarkable electrical and optical switching properties induced at low power and near room temperature (68C), vanadium dioxide (VO2) has sparked rising interest in unconventional computing among the phase-change materials research community. The scalability and the potential to compute beyond the von Neumann model make VO2 especially appealing for implementation in oscillating neural networks for artificial intelligence (AI) applications, to solve constraint satisfaction problems, and for pattern recognition. Its integration into large networks of oscillators on a Silicon platform still poses challenges associated with the stabilization in the correct oxidation state and the ability to fabricate a structure with predictable electrical behavior showing very low variability. In this work, the role played by the different annealing parameters applied by three methods (slow thermal annealing, flash annealing, and rapid thermal annealing), following the vanadium oxide atomic layer deposition (ALD), on the formation of VO2 grains is studied and an optimal substrate stack configuration that minimizes variability between devices is proposed. Material and electrical characterizations are performed on the different films and a step-by-step recipe to build reproducible VO2-based oscillators is presented, which is argued to be made possible thanks to the introduction of a hafnium oxide (HfO2) layer between the silicon substrate and the vanadium oxide layer. Up to seven nearly identical VO2-based devices are contacted simultaneously to create a network of oscillators, paving the way for large-scale implementation of VO2 oscillating neural networks. △ Less

Submitted 13 May, 2024; v1 submitted 5 March, 2024; originally announced March 2024.

SynthScribe: Deep Multimodal Tools for Synthesizer Sound Retrieval and Exploration

Authors: Stephen Brade, Bryan Wang, Mauricio Sousa, Gregory Lee Newsome, Sageev Oore, Tovi Grossman

Abstract: Synthesizers are powerful tools that allow musicians to create dynamic and original sounds. Existing commercial interfaces for synthesizers typically require musicians to interact with complex low-level parameters or to manage large libraries of premade sounds. To address these challenges, we implement SynthScribe -- a fullstack system that uses multimodal deep learning to let users express their… ▽ More Synthesizers are powerful tools that allow musicians to create dynamic and original sounds. Existing commercial interfaces for synthesizers typically require musicians to interact with complex low-level parameters or to manage large libraries of premade sounds. To address these challenges, we implement SynthScribe -- a fullstack system that uses multimodal deep learning to let users express their intentions at a much higher level. We implement features which address a number of difficulties, namely 1) searching through existing sounds, 2) creating completely new sounds, 3) making meaningful modifications to a given sound. This is achieved with three main features: a multimodal search engine for a large library of synthesizer sounds; a user centered genetic algorithm by which completely new sounds can be created and selected given the users preferences; a sound editing support feature which highlights and gives examples for key control parameters with respect to a text or audio based query. The results of our user studies show SynthScribe is capable of reliably retrieving and modifying sounds while also affording the ability to create completely new sounds that expand a musicians creative horizon. △ Less

Submitted 20 February, 2024; v1 submitted 7 December, 2023; originally announced December 2023.

Geo-Sketcher: Rapid 3D Geological Modeling using Geological and Topographic Map Sketches

Authors: Ronan Amorim, Emilio Vital Brazil, Faramarz Samavati, Mario Costa Sousa

Abstract: The construction of 3D geological models is an essential task in oil/gas exploration, development and production. However, it is a cumbersome, time-consuming and error-prone task mainly because of the model's geometric and topological complexity. The models construction is usually separated into interpretation and 3D modeling, performed by different highly specialized individuals, which leads to i… ▽ More The construction of 3D geological models is an essential task in oil/gas exploration, development and production. However, it is a cumbersome, time-consuming and error-prone task mainly because of the model's geometric and topological complexity. The models construction is usually separated into interpretation and 3D modeling, performed by different highly specialized individuals, which leads to inconsistencies and intensifies the challenges. In addition, the creation of models following geological rules is paramount for properly depicting static and dynamic properties of oil/gas reservoirs. In this work, we propose a sketch-based approach to expedite the creation of valid 3D geological models by mimicking how domain experts interpret geological structures, allowing creating models directly from interpretation sketches. Our sketch-based modeler (Geo-Sketcher) is based on sketches of standard 2D topographic and geological maps, comprised of lines, symbols and annotations. We developed a graph-based representation to enable (1) the automatic computation of the relative ages of rock series and layers, and (2) the embedding of specific geological rules directly in the sketching. We introduce the use of Hermite-Birkhoff Radial Basis Functions to interpolate the geological map constraints, and demonstrate the capabilities of our approach with a variety of results with different levels of complexity. △ Less

Submitted 21 August, 2023; originally announced August 2023.

Comments: 21 pages, 30 Figures

Building Flyweight FLIM-based CNNs with Adaptive Decoding for Object Detection

Authors: Leonardo de Melo Joao, Azael de Melo e Sousa, Bianca Martins dos Santos, Silvio Jamil Ferzoli Guimaraes, Jancarlo Ferreira Gomes, Ewa Kijak, Alexandre Xavier Falcao

Abstract: State-of-the-art (SOTA) object detection methods have succeeded in several applications at the price of relying on heavyweight neural networks, which makes them inefficient and inviable for many applications with computational resource constraints. This work presents a method to build a Convolutional Neural Network (CNN) layer by layer for object detection from user-drawn markers on discriminative… ▽ More State-of-the-art (SOTA) object detection methods have succeeded in several applications at the price of relying on heavyweight neural networks, which makes them inefficient and inviable for many applications with computational resource constraints. This work presents a method to build a Convolutional Neural Network (CNN) layer by layer for object detection from user-drawn markers on discriminative regions of representative images. We address the detection of Schistosomiasis mansoni eggs in microscopy images of fecal samples, and the detection of ships in satellite images as application examples. We could create a flyweight CNN without backpropagation from very few input images. Our method explores a recent methodology, Feature Learning from Image Markers (FLIM), to build convolutional feature extractors (encoders) from marker pixels. We extend FLIM to include a single-layer adaptive decoder, whose weights vary with the input image -- a concept never explored in CNNs. Our CNN weighs thousands of times less than SOTA object detectors, being suitable for CPU execution and showing superior or equivalent performance to three methods in five measures. △ Less

Submitted 5 October, 2023; v1 submitted 26 June, 2023; originally announced June 2023.

Promptify: Text-to-Image Generation through Interactive Prompt Exploration with Large Language Models

Authors: Stephen Brade, Bryan Wang, Mauricio Sousa, Sageev Oore, Tovi Grossman

Abstract: Text-to-image generative models have demonstrated remarkable capabilities in generating high-quality images based on textual prompts. However, crafting prompts that accurately capture the user's creative intent remains challenging. It often involves laborious trial-and-error procedures to ensure that the model interprets the prompts in alignment with the user's intention. To address the challenges… ▽ More Text-to-image generative models have demonstrated remarkable capabilities in generating high-quality images based on textual prompts. However, crafting prompts that accurately capture the user's creative intent remains challenging. It often involves laborious trial-and-error procedures to ensure that the model interprets the prompts in alignment with the user's intention. To address the challenges, we present Promptify, an interactive system that supports prompt exploration and refinement for text-to-image generative models. Promptify utilizes a suggestion engine powered by large language models to help users quickly explore and craft diverse prompts. Our interface allows users to organize the generated images flexibly, and based on their preferences, Promptify suggests potential changes to the original prompt. This feedback loop enables users to iteratively refine their prompts and enhance desired features while avoiding unwanted ones. Our user study shows that Promptify effectively facilitates the text-to-image workflow and outperforms an existing baseline tool widely used for text-to-image generation. △ Less

Submitted 18 April, 2023; originally announced April 2023.

Carolina: a General Corpus of Contemporary Brazilian Portuguese with Provenance, Typology and Versioning Information

Authors: Maria Clara Ramos Morales Crespo, Maria Lina de Souza Jeannine Rocha, Mariana Lourenço Sturzeneker, Felipe Ribas Serras, Guilherme Lamartine de Mello, Aline Silva Costa, Mayara Feliciano Palma, Renata Morais Mesquita, Raquel de Paula Guets, Mariana Marques da Silva, Marcelo Finger, Maria Clara Paixão de Sousa, Cristiane Namiuti, Vanessa Martins do Monte

Abstract: This paper presents the first publicly available version of the Carolina Corpus and discusses its future directions. Carolina is a large open corpus of Brazilian Portuguese texts under construction using web-as-corpus methodology enhanced with provenance, typology, versioning, and text integrality. The corpus aims at being used both as a reliable source for research in Linguistics and as an import… ▽ More This paper presents the first publicly available version of the Carolina Corpus and discusses its future directions. Carolina is a large open corpus of Brazilian Portuguese texts under construction using web-as-corpus methodology enhanced with provenance, typology, versioning, and text integrality. The corpus aims at being used both as a reliable source for research in Linguistics and as an important resource for Computer Science research on language models, contributing towards removing Portuguese from the set of low-resource languages. Here we present the construction of the corpus methodology, comparing it with other existing methodologies, as well as the corpus current state: Carolina's first public version has $653,322,577$ tokens, distributed over $7$ broad types. Each text is annotated with several different metadata categories in its header, which we developed using TEI annotation standards. We also present ongoing derivative works and invite NLP researchers to contribute with their own. △ Less

Submitted 28 March, 2023; originally announced March 2023.

Comments: 14 pages, 3 figures, 1 appendix

MSC Class: 68T50 ACM Class: I.2.7

Stargazer: An Interactive Camera Robot for Capturing How-To Videos Based on Subtle Instructor Cues

Authors: Jiannan Li, Mauricio Sousa, Karthik Mahadevan, Bryan Wang, Paula Akemi Aoyaui, Nicole Yu, Angela Yang, Ravin Balakrishnan, Anthony Tang, Tovi Grossman

Abstract: Live and pre-recorded video tutorials are an effective means for teaching physical skills such as cooking or prototy** electronics. A dedicated cameraperson following an instructor's activities can improve production quality. However, instructors who do not have access to a cameraperson's help often have to work within the constraints of static cameras. We present Stargazer, a novel approach for… ▽ More Live and pre-recorded video tutorials are an effective means for teaching physical skills such as cooking or prototy** electronics. A dedicated cameraperson following an instructor's activities can improve production quality. However, instructors who do not have access to a cameraperson's help often have to work within the constraints of static cameras. We present Stargazer, a novel approach for assisting with tutorial content creation with a camera robot that autonomously tracks regions of interest based on instructor actions to capture dynamic shots. Instructors can adjust the camera behaviors of Stargazer with subtle cues, including gestures and speech, allowing them to fluidly integrate camera control commands into instructional activities. Our user study with six instructors, each teaching a distinct skill, showed that participants could create dynamic tutorial videos with a diverse range of subjects, camera framing, and camera angle combinations using Stargazer. △ Less

Submitted 6 March, 2023; originally announced March 2023.

Comments: To appear in Proceedings of the 2023 CHI Conference on Human Factors in Computing Systems (CHI '23), April 23--28, 2023, Hamburg, Germany

MAGIC: Manipulating Avatars and Gestures to Improve Remote Collaboration

Authors: Catarina G. Fidalgo, Maurício Sousa, Daniel Mendes, Rafael Kuffner dos Anjos, Daniel Medeiros, Karan Singh, Joaquim Jorge

Abstract: Remote collaborative work has become pervasive in many settings, from engineering to medical professions. Users are immersed in virtual environments and communicate through life-sized avatars that enable face-to-face collaboration. Within this context, users often collaboratively view and interact with virtual 3D models, for example, to assist in designing new devices such as customized prosthetic… ▽ More Remote collaborative work has become pervasive in many settings, from engineering to medical professions. Users are immersed in virtual environments and communicate through life-sized avatars that enable face-to-face collaboration. Within this context, users often collaboratively view and interact with virtual 3D models, for example, to assist in designing new devices such as customized prosthetics, vehicles, or buildings. However, discussing shared 3D content face-to-face has various challenges, such as ambiguities, occlusions, and different viewpoints that all decrease mutual awareness, leading to decreased task performance and increased errors. To address this challenge, we introduce MAGIC, a novel approach for understanding pointing gestures in a face-to-face shared 3D space, improving mutual understanding and awareness. Our approach distorts the remote userś gestures to correctly reflect them in the local userś reference space when face-to-face. We introduce a novel metric called pointing agreement to measure what two users perceive in common when using pointing gestures in a shared 3D space. Results from a user study suggest that MAGIC significantly improves pointing agreement in face-to-face collaboration settings, improving co-presence and awareness of interactions performed in the shared space. We believe that MAGIC improves remote collaboration by enabling simpler communication mechanisms and better mutual awareness. △ Less

Submitted 15 February, 2023; originally announced February 2023.

Comments: Presented at IEEE VR 2023

A general framework for multi-step ahead adaptive conformal heteroscedastic time series forecasting

Authors: Martim Sousa, Ana Maria Tomé, José Moreira

Abstract: This paper introduces a novel model-agnostic algorithm called adaptive ensemble batch multi-input multi-output conformalized quantile regression (AEnbMIMOCQR} that enables forecasters to generate multi-step ahead prediction intervals for a fixed pre-specified miscoverage rate in a distribution-free manner. Our method is grounded on conformal prediction principles, however, it does not require data… ▽ More This paper introduces a novel model-agnostic algorithm called adaptive ensemble batch multi-input multi-output conformalized quantile regression (AEnbMIMOCQR} that enables forecasters to generate multi-step ahead prediction intervals for a fixed pre-specified miscoverage rate in a distribution-free manner. Our method is grounded on conformal prediction principles, however, it does not require data splitting and provides close to exact coverage even when the data is not exchangeable. Moreover, the resulting prediction intervals, besides being empirically valid along the forecast horizon, do not neglect heteroscedasticity. AEnbMIMOCQR is designed to be robust to distribution shifts, which means that its prediction intervals remain reliable over an unlimited period of time, without entailing retraining or imposing unrealistic strict assumptions on the data-generating process. Through methodically experimentation, we demonstrate that our approach outperforms other competitive methods on both real-world and synthetic datasets. The code used in the experimental part and a tutorial on how to use AEnbMIMOCQR can be found at the following GitHub repository: https://github.com/Quilograma/AEnbMIMOCQR. △ Less

Submitted 11 October, 2023; v1 submitted 28 July, 2022; originally announced July 2022.

Comments: 34 pages, 8 figures

Improved conformalized quantile regression

Authors: Martim Sousa, Ana Maria Tomé, José Moreira

Abstract: Conformalized quantile regression is a procedure that inherits the advantages of conformal prediction and quantile regression. That is, we use quantile regression to estimate the true conditional quantile and then apply a conformal step on a calibration set to ensure marginal coverage. In this way, we get adaptive prediction intervals that account for heteroscedasticity. However, the aforementione… ▽ More Conformalized quantile regression is a procedure that inherits the advantages of conformal prediction and quantile regression. That is, we use quantile regression to estimate the true conditional quantile and then apply a conformal step on a calibration set to ensure marginal coverage. In this way, we get adaptive prediction intervals that account for heteroscedasticity. However, the aforementioned conformal step lacks adaptiveness as described in (Romano et al., 2019). To overcome this limitation, instead of applying a single conformal step after estimating conditional quantiles with quantile regression, we propose to cluster the explanatory variables weighted by their permutation importance with an optimized k-means and apply k conformal steps. To show that this improved version outperforms the classic version of conformalized quantile regression and is more adaptive to heteroscedasticity, we extensively compare the prediction intervals of both in open datasets. △ Less

Submitted 6 November, 2022; v1 submitted 6 July, 2022; originally announced July 2022.

Comments: 11 pages, 10 figures

Inductive Conformal Prediction: A Straightforward Introduction with Examples in Python

Authors: Martim Sousa

Abstract: Inductive Conformal Prediction (ICP) is a set of distribution-free and model agnostic algorithms devised to predict with a user-defined confidence with coverage guarantee. Instead of having point predictions, i.e., a real number in the case of regression or a single class in multi class classification, models calibrated using ICP output an interval or a set of classes, respectively. ICP takes spec… ▽ More Inductive Conformal Prediction (ICP) is a set of distribution-free and model agnostic algorithms devised to predict with a user-defined confidence with coverage guarantee. Instead of having point predictions, i.e., a real number in the case of regression or a single class in multi class classification, models calibrated using ICP output an interval or a set of classes, respectively. ICP takes special importance in high-risk settings where we want the true output to belong to the prediction set with high probability. As an example, a classification model might output that given a magnetic resonance image a patient has no latent diseases to report. However, this model output was based on the most likely class, the second most likely class might tell that the patient has a 15% chance of brain tumor or other severe disease and therefore further exams should be conducted. Using ICP is therefore way more informative and we believe that should be the standard way of producing forecasts. This paper is a hands-on introduction, this means that we will provide examples as we introduce the theory. △ Less

Submitted 1 July, 2022; v1 submitted 23 June, 2022; originally announced June 2022.

Comments: 6 pages, 11 figures, tutorial

Roadblocks to Attracting Students to Software Testing Careers: Comparisons of Replicated Studies

Authors: Rodrigo E. C. Souza, Ronnie E. de Souza Santos, Luiz Fernando Capretz, Marlon A. S. de Sousa, Cleyton V. C. de Magalhaes

Abstract: Context. Recently, a family of studies highlighted the unpopularity of software testing careers among undergraduate students in software engineering and computer science courses. The original study and its replications explored the perception of students in universities in four countries (Cana-da, China, India, and Malaysia), and indicated that most students do not consider a career in software te… ▽ More Context. Recently, a family of studies highlighted the unpopularity of software testing careers among undergraduate students in software engineering and computer science courses. The original study and its replications explored the perception of students in universities in four countries (Cana-da, China, India, and Malaysia), and indicated that most students do not consider a career in software testing as an option after graduation. This scenario represents a problem for the software industry since the lack of skilled testing professionals might decrease the quality of software projects and increase the number of unsuccessful projects. Goal. The present study aims to replicate, in Brazil, the studies conducted in the other four countries to establish comparisons and support the development of strategies to improve the visibility and importance of software testing among undergraduate students across the globe. Method. We followed the same protocol in the original study to collect data using a questionnaire and analyzed the answers using descriptive statistics and qualitative data analysis. Results. Our findings indicate similarities among the results obtained in Brazil in comparison to those obtained from other countries. We observed that students are not motivated to follow a testing career in the software industry based on a belief that testing activities lack challenges and opportunities for continuous learning. Conclusions. In summary, students seem to be interested in learning more about software testing. However, the lack of discussions about the theme in software development courses, as well as the limited offer of courses focused on software quality at the university level reduce the visibility of this area, which causes a decrease in the interest in this career. △ Less

Submitted 15 June, 2022; originally announced June 2022.

Anatomy Studio II: A Cross-Reality Application for Teaching Anatomy

Authors: Joaquim Jorge, Pedro Belchior, Abel Gomes, Maurício Sousa, João Pereira, Jean-François Uhl

Abstract: Virtual Reality has become an important educational tool, due to the pandemic and increasing globalization of education. This paper presents a framework for teaching Virtual Anatomy at the university level. Virtual classes have become a staple of today's curricula because of the isolation and quarantine requirements and the increased international collaboration. Our work builds on the Visible Huma… ▽ More Virtual Reality has become an important educational tool, due to the pandemic and increasing globalization of education. This paper presents a framework for teaching Virtual Anatomy at the university level. Virtual classes have become a staple of today's curricula because of the isolation and quarantine requirements and the increased international collaboration. Our work builds on the Visible Human Projects for Virtual Dissection material and provides a medium for groups of students to do collaborative anatomical dissections in real-time using sketching and 3D visualizations and audio coupled with interactive 2D tablets for precise drawing. We describe the system architecture, compare requirements with those of previous development, and discuss the preliminary results. Discussions with Anatomists show that this is an effective tool. We introduce avenues for further research and discuss collaboration challenges posed by this context. △ Less

Submitted 4 March, 2022; originally announced March 2022.

Comments: 4 pages

ACM Class: I.3; J.3

Design requirements to improve laparoscopy via XR

Authors: Ezequiel R. Zorzal, Maurício Sousa, Pedro Belchior, João Madeiras Pereira, Nuno Figueiredo, Joaquim Jorge

Abstract: Laparoscopic surgery has the advantage of avoiding large open incisions and thereby decreasing blood loss, pain, and discomfort to patients. However, on the other side, it is hampered by restricted workspace, ambiguous communication, and surgeon fatigue caused by non-ergonomic head positioning. We aimed to identify critical problems and suggest design requirements and solutions. We used user and t… ▽ More Laparoscopic surgery has the advantage of avoiding large open incisions and thereby decreasing blood loss, pain, and discomfort to patients. However, on the other side, it is hampered by restricted workspace, ambiguous communication, and surgeon fatigue caused by non-ergonomic head positioning. We aimed to identify critical problems and suggest design requirements and solutions. We used user and task analysis methods to learn about practices performed in an operating room by observing surgeons in their working environment to understand how they performed tasks and achieved their intended goals. Drawing on observations and analysis from recorded laparoscopic surgeries, we have identified several constraints and design requirements to propose potential solutions to address the issues. Surgeons operate in a dimly lit environment, surrounded by monitors, and communicate through verbal commands and pointing gestures. Therefore, performing user and task analysis allowed us to better understand the existing problems in laparoscopy while identifying several communication constraints and design requirements, which a solution has to follow to address those problems. Our contributions include identifying design requirements for laparoscopy surgery through a user and task analysis. These requirements propose design solutions towards improved surgeons' comfort and make the surgical procedure less laborious. △ Less

Submitted 3 March, 2022; originally announced March 2022.

Comments: 5 pages, 7 figures, workshop paper

ACM Class: I.3; J.3

A Flexible HLS Hoeffding Tree Implementation for Runtime Learning on FPGA

Authors: Luís Miguel Sousa, Nuno Paulino, João Canas Ferreira, João Bispo

Abstract: Decision trees are often preferred when implementing Machine Learning in embedded systems for their simplicity and scalability. Hoeffding Trees are a type of Decision Trees that take advantage of the Hoeffding Bound to allow them to learn patterns in data without having to continuously store the data samples for future reprocessing. This makes them especially suitable for deployment on embedded de… ▽ More Decision trees are often preferred when implementing Machine Learning in embedded systems for their simplicity and scalability. Hoeffding Trees are a type of Decision Trees that take advantage of the Hoeffding Bound to allow them to learn patterns in data without having to continuously store the data samples for future reprocessing. This makes them especially suitable for deployment on embedded devices. In this work we highlight the features of an HLS implementation of the Hoeffding Tree. The implementation parameters include the feature size of the samples (D), the number of output classes (K), and the maximum number of nodes to which the tree is allowed to grow (Nd). We target a Xilinx MPSoC ZCU102, and evaluate: the design's resource requirements and clock frequency for different numbers of classes and feature size, the execution time on several synthetic datasets of varying sample sizes (N), number of output classes and the execution time and accuracy for two datasets from UCI. For a problem size of D3, K5, and N40000, a single decision tree operating at 103MHz is capable of 8.3x faster inference than the 1.2GHz ARM Cortex-A53 core. Compared to a reference implementation of the Hoeffding tree, we achieve comparable classification accuracy for the UCI datasets. △ Less

Submitted 3 December, 2021; originally announced December 2021.

CNN Filter Learning from Drawn Markers for the Detection of Suggestive Signs of COVID-19 in CT Images

Authors: Azael M. Sousa, Fabiano Reis, Rachel Zerbini, João L. D. Comba, Alexandre X. Falcão

Abstract: Early detection of COVID-19 is vital to control its spread. Deep learning methods have been presented to detect suggestive signs of COVID-19 from chest CT images. However, due to the novelty of the disease, annotated volumetric data are scarce. Here we propose a method that does not require either large annotated datasets or backpropagation to estimate the filters of a convolutional neural network… ▽ More Early detection of COVID-19 is vital to control its spread. Deep learning methods have been presented to detect suggestive signs of COVID-19 from chest CT images. However, due to the novelty of the disease, annotated volumetric data are scarce. Here we propose a method that does not require either large annotated datasets or backpropagation to estimate the filters of a convolutional neural network (CNN). For a few CT images, the user draws markers at representative normal and abnormal regions. The method generates a feature extractor composed of a sequence of convolutional layers, whose kernels are specialized in enhancing regions similar to the marked ones, and the decision layer of our CNN is a support vector machine. As we have no control over the CT image acquisition, we also propose an intensity standardization approach. Our method can achieve mean accuracy and kappa values of $0.97$ and $0.93$, respectively, on a dataset with 117 CT images extracted from different sites, surpassing its counterpart in all scenarios. △ Less

Submitted 16 November, 2021; originally announced November 2021.

Comments: 4 pages. To be published in the 43rd Annual International Conference of the IEEE Engineering in Medicine and Biology Society

ACM Class: J.3, J.6

"Grip-that-there": An Investigation of Explicit and Implicit Task Allocation Techniques for Human-Robot Collaboration

Authors: Karthik Mahadevan, Maurício Sousa, Anthony Tang, Tovi Grossman

Abstract: In ad-hoc human-robot collaboration (HRC), humans and robots work on a task without pre-planning the robot's actions prior to execution; instead, task allocation occurs in real-time. However, prior research has largely focused on task allocations that are pre-planned - there has not been a comprehensive exploration or evaluation of techniques where task allocation is adjusted in real-time. Inspire… ▽ More In ad-hoc human-robot collaboration (HRC), humans and robots work on a task without pre-planning the robot's actions prior to execution; instead, task allocation occurs in real-time. However, prior research has largely focused on task allocations that are pre-planned - there has not been a comprehensive exploration or evaluation of techniques where task allocation is adjusted in real-time. Inspired by HCI research on territoriality and proxemics, we propose a design space of novel task allocation techniques including both explicit techniques, where the user maintains agency, and implicit techniques, where the efficiency of automation can be leveraged. The techniques were implemented and evaluated using a tabletop HRC simulation in VR. A 16-participant study, which presented variations of a collaborative block stacking task, showed that implicit techniques enable efficient task completion and task parallelization, and should be augmented with explicit mechanisms to provide users with fine-grained control. △ Less

Submitted 2 February, 2021; v1 submitted 31 January, 2021; originally announced February 2021.

Comments: To be published in Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems

ACM Class: H.5.2

Adamastor: a New Low Latency and Scalable Decentralized Anonymous Payment System

Authors: Rui Morais, Paul Crocker, Simao Melo de Sousa

Abstract: This paper presents Adamastor, a new low latency and scalable decentralized anonymous payment system, which is an extension of Ring Confidential Transactions (RingCT) that is compatible with consensus algorithms that use Delegated Proof of Stake (DPoS) as a defense mechanism against Sybil attacks. Adamastor also includes a new Decoy Selection Algorithm (DSA) that can be of independent interest, ca… ▽ More This paper presents Adamastor, a new low latency and scalable decentralized anonymous payment system, which is an extension of Ring Confidential Transactions (RingCT) that is compatible with consensus algorithms that use Delegated Proof of Stake (DPoS) as a defense mechanism against Sybil attacks. Adamastor also includes a new Decoy Selection Algorithm (DSA) that can be of independent interest, called SimpleDSA, a crucial aspect of protocols that use ring signatures to anonymize the sender. SimpleDSA offers security against homogeneity attacks and chain analysis. Moreover, it enables the pruning of spent outputs, addressing the issue of perpetual output growth commonly associated with such schemes. Adamastor is implemented and evaluated using the Narwhal consensus algorithm, demonstrating significantly lower latency compared to Proof of Work based cryptocurrencies. Adamastor also exhibits ample scalability, making it suitable for a decentralized and anonymous payment network. △ Less

Submitted 14 December, 2023; v1 submitted 28 November, 2020; originally announced November 2020.

Learning-based Defect Recognition for Quasi-Periodic Microscope Images

Authors: Nik Dennler, Antonio Foncubierta-Rodriguez, Titus Neupert, Marilyne Sousa

Abstract: Controlling crystalline material defects is crucial, as they affect properties of the material that may be detrimental or beneficial for the final performance of a device. Defect analysis on the sub-nanometer scale is enabled by high-resolution (scanning) transmission electron microscopy [HR(S)TEM], where the identification of defects is currently carried out based on human expertise. However, the… ▽ More Controlling crystalline material defects is crucial, as they affect properties of the material that may be detrimental or beneficial for the final performance of a device. Defect analysis on the sub-nanometer scale is enabled by high-resolution (scanning) transmission electron microscopy [HR(S)TEM], where the identification of defects is currently carried out based on human expertise. However, the process is tedious, highly time consuming and, in some cases, yields ambiguous results. Here we propose a semi-supervised machine learning method that assists in the detection of lattice defects from atomic resolution microscope images. It involves a convolutional neural network that classifies image patches as defective or non-defective, a graph-based heuristic that chooses one non-defective patch as a model, and finally an automatically generated convolutional filter bank, which highlights symmetry breaking such as stacking faults, twin defects and grain boundaries. Additionally, we suggest a variance filter to segment amorphous regions and beam defects. The algorithm is tested on III-V/Si crystalline materials and successfully evaluated against different metrics, showing promising results even for extremely small training data sets. By combining the data-driven classification generality, robustness and speed of deep learning with the effectiveness of image filters in segmenting faulty symmetry arrangements, we provide a valuable open-source tool to the microscopist community that can streamline future HR(S)TEM analyses of crystalline materials. △ Less

Submitted 9 August, 2020; v1 submitted 2 July, 2020; originally announced July 2020.

Comments: 11 pages + references and appendix, 5 figures. V2: Added references. Corrected typos. Elaborated methodology. In sample figure, replaced grain boundary image with more representative image. Results are unchanged

WhylSon: Proving your Michelson Smart Contracts in Why3

Authors: Luís Pedro Arrojado da Horta, João Santos Reis, Mário Pereira, Simão Melo de Sousa

Abstract: This paper introduces WhylSon, a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. WhylSon accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework. Smart contract instructions are mapped into… ▽ More This paper introduces WhylSon, a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain. WhylSon accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework. Smart contract instructions are mapped into a corresponding WhyML shallow-embedding of the their axiomatic semantics, which we also developed in the context of this work. One major advantage of this approach is that it allows an out-of-the-box integration with the Why3 framework, namely its VCGen and the backend support for several automated theorem provers. We also discuss the use of WhylSon to automatically prove the correctness of diverse annotated smart contracts. △ Less

Submitted 29 May, 2020; originally announced May 2020.

Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts

Authors: João Santos Reis, Paul Crocker, Simão Melo de Sousa

Abstract: This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and preserves the semantics, ow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smar… ▽ More This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and preserves the semantics, ow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smart contracts to Tezla. In order to support our claim about the adequacy of Tezla, we develop a static analyser that takes advantage of the Tezla representation of Michelson smart contracts to prove simple but non-trivial properties. △ Less

Submitted 24 May, 2020; originally announced May 2020.

A back-end, CMOS compatible ferroelectric Field Effect Transistor for synaptic weights

Authors: Mattia Halter, Laura Bégon-Lours, Valeria Bragaglia, Marilyne Sousa, Bert Jan Offrein, Stefan Abel, Mathieu Luisier, Jean Fompeyriney

Abstract: Neuromorphic computing architectures enable the dense co-location of memory and processing elements within a single circuit. This co-location removes the communication bottleneck of transferring data between separate memory and computing units as in standard von Neuman architectures for data-critical applications including machine learning. The essential building blocks of neuromorphic systems are… ▽ More Neuromorphic computing architectures enable the dense co-location of memory and processing elements within a single circuit. This co-location removes the communication bottleneck of transferring data between separate memory and computing units as in standard von Neuman architectures for data-critical applications including machine learning. The essential building blocks of neuromorphic systems are non-volatile synaptic elements such as memristors. Key memristor properties include a suitable non-volatile resistance range, continuous linear resistance modulation and symmetric switching. In this work, we demonstrate voltage-controlled, symmetric and analog potentiation and depression of a ferroelectric Hf$_{57}$Zr$_{43}$O$_{2}$ (HZO) field effect transistor (FeFET) with good linearity. Our FeFET operates with a low writing energy (fJ) and fast programming time (40 ns). Retention measurements have been done over 4-bits depth with low noise (1%) in the tungsten oxide (WO$_{x}$) read out channel. By adjusting the channel thickness from 15nm to 8nm, the on/off ratio of the FeFET can be engineered from 1% to 200% with an on-resistance ideally >100 kOhm, depending on the channel geometry. The device concept is using earth-abundant materials, and is compatible with a back end of line (BEOL) integration into complementary metal-oxidesemiconductor (CMOS) processes. It has therefore a great potential for the fabrication of high density, large-scale integrated arrays of artificial analog synapses. △ Less

Submitted 17 January, 2020; originally announced January 2020.

Comments: 14 pages, 5 figures, supplementary information available, submitted to ACS Applied Materials & Interfaces

Safe Walking In VR using Augmented Virtuality

Authors: Maurício Sousa, Daniel Mendes, Joaquim Jorge

Abstract: New technologies allow ordinary people to access Virtual Reality at affordable prices in their homes. One of the most important tasks when interacting with immersive Virtual Reality is to navigate the virtual environments (VEs). Arguably, the best methods to accomplish this use of direct control interfaces. Among those, natural walking (NW) makes for enjoyable user experience. However, common tech… ▽ More New technologies allow ordinary people to access Virtual Reality at affordable prices in their homes. One of the most important tasks when interacting with immersive Virtual Reality is to navigate the virtual environments (VEs). Arguably, the best methods to accomplish this use of direct control interfaces. Among those, natural walking (NW) makes for enjoyable user experience. However, common techniques to support direct control interfaces in VEs feature constraints that make it difficult to use those methods in cramped home environments. Indeed, NW requires unobstructed and open space. To approach this problem, we propose a new virtual locomotion technique, Combined Walking in Place (CWIP). CWIP allows people to take advantage of the available physical space and empowers them to use NW to navigate in the virtual world. For longer distances, we adopt Walking in Place (WIP) to enable them to move in the virtual world beyond the confines of a cramped real room. However, roaming in immersive alternate reality, while moving in the confines of a cluttered environment can lead people to stumble and fall. To approach these problems, we developed Augmented Virtual Reality (AVR), to inform users about real-world hazards, such as chairs, drawers, walls via proxies and signs placed in the virtual world. We propose thus CWIP-AVR as a way to safely explore VR in the cramped confines of your own home. To our knowledge, this is the first approach to combined different locomotion modalities in a safe manner. We evaluated it in a user study with 20 participants to validate their ability to navigate a virtual world while walking in a confined and cluttered real space. Our results show that CWIP-AVR allows people to navigate VR safely, switching between locomotion modes flexibly while maintaining a good immersion. △ Less

Submitted 29 November, 2019; originally announced November 2019.

Comments: 10 pages, 10 figures, VRCAI 2019 Poster; The Authors would like to thank Francisco Venda for his work and contributions

Negative Space: Workspace Awareness in 3D Face-to-Face Remote Collaboration

Authors: Maurício Sousa, Daniel Mendes, Rafael Kuffner dos Anjos, Daniel Simões Lopes, Joaquim Jorge

Abstract: Face-to-face telepresence promotes the sense of "being there" and can improve collaboration by allowing immediate understanding of remote people's nonverbal cues. Several approaches successfully explored interactions with 2D content using a see-through whiteboard metaphor. However, with 3D content, there is a decrease in awareness due to ambiguities originated by participants' opposing points-of-v… ▽ More Face-to-face telepresence promotes the sense of "being there" and can improve collaboration by allowing immediate understanding of remote people's nonverbal cues. Several approaches successfully explored interactions with 2D content using a see-through whiteboard metaphor. However, with 3D content, there is a decrease in awareness due to ambiguities originated by participants' opposing points-of-view. In this paper, we investigate how people and content should be presented for discussing 3D renderings within face-to-face collaborative sessions. To this end, we performed a user evaluation to compare four different conditions, in which we varied reflections of both workspace and remote people representation. Results suggest potentially more benefits to remote collaboration from workspace consistency rather than people's representation fidelity. We contribute a novel design space, the Negative Space, for remote face-to-face collaboration focusing on 3D content. △ Less

Submitted 8 October, 2019; originally announced October 2019.

Verifying Semantic Conflict-Freedom in Three-Way Program Merges

Authors: Marcelo Sousa, Isil Dillig, Shuvendu Lahiri

Abstract: Even though many programmers rely on 3-way merge tools to integrate changes from different branches, such tools can introduce subtle bugs in the integration process. This paper aims to mitigate this problem by defining a semantic notion of confict-freedom, which ensures that the merged program does not introduce new unwanted behaviors. We also show how to verify this property using a novel, compos… ▽ More Even though many programmers rely on 3-way merge tools to integrate changes from different branches, such tools can introduce subtle bugs in the integration process. This paper aims to mitigate this problem by defining a semantic notion of confict-freedom, which ensures that the merged program does not introduce new unwanted behaviors. We also show how to verify this property using a novel, compositional algorithm that combines lightweight dependence analysis for shared program fragments and precise relational reasoning for the modifications. We evaluate our tool called SafeMerge on 52 real-world merge scenarios obtained from Github and compare the results against a textual merge tool. The experimental results demonstrate the benefits of our approach over syntactic confict-freedom and indicate that SafeMerge is both precise and practical. △ Less

Submitted 19 February, 2018; originally announced February 2018.

Quasi-Optimal Partial Order Reduction

Authors: Huyen T. T Nguyen, César Rodríguez, Marcelo Sousa, Camille Coti, Laure Petrucci

Abstract: A dynamic partial order reduction (DPOR) algorithm is optimal when it always explores at most one representative per Mazurkiewicz trace. Existing literature suggests that the reduction obtained by the non-optimal, state-of-the-art Source-DPOR (SDPOR) algorithm is comparable to optimal DPOR. We show the first program with $\mathop{\mathcal{O}}(n)$ Mazurkiewicz traces where SDPOR explores… ▽ More A dynamic partial order reduction (DPOR) algorithm is optimal when it always explores at most one representative per Mazurkiewicz trace. Existing literature suggests that the reduction obtained by the non-optimal, state-of-the-art Source-DPOR (SDPOR) algorithm is comparable to optimal DPOR. We show the first program with $\mathop{\mathcal{O}}(n)$ Mazurkiewicz traces where SDPOR explores $\mathop{\mathcal{O}}(2^n)$ redundant schedules and identify the cause of the blow-up as an NP-hard problem. Our main contribution is a new approach, called Quasi-Optimal POR, that can arbitrarily approximate an optimal exploration using a provided constant k. We present an implementation of our method in a new tool called Dpu using specialised data structures. Experiments with Dpu, including Debian packages, show that optimality is achieved with low values of k, outperforming state-of-the-art tools. △ Less

Submitted 20 April, 2018; v1 submitted 12 February, 2018; originally announced February 2018.

Comments: Minor corrections after review for publication

Revisiting concurrent separation logic

Authors: Pedro Soares, António Ravara, Simão Melo de Sousa

Abstract: We present a new soundness proof of Concurrent Separation Logic (CSL) based on a structural operational semantics (SOS). We build on two previous proofs and develop new auxiliary notions to achieve the goal. One uses a denotational semantics (based on traces). The other is based on SOS, but was obtained only for a fragment of the logic - the Disjoint CSL - which disallows modifying shared variable… ▽ More We present a new soundness proof of Concurrent Separation Logic (CSL) based on a structural operational semantics (SOS). We build on two previous proofs and develop new auxiliary notions to achieve the goal. One uses a denotational semantics (based on traces). The other is based on SOS, but was obtained only for a fragment of the logic - the Disjoint CSL - which disallows modifying shared variables between concurrent threads. In this work, we lift such a restriction, proving the soundness of full CSL with respect to a SOS. Thus contributing to the development of tools able of ensuring the correctness of realistic concurrent programs. Moreover, given that we used SOS, such tools can be well-integrated in programming environments and even incorporated in compilers. △ Less

Submitted 5 December, 2017; originally announced December 2017.

Journal ref: Journal of Logical and Algebraic Methods in Programming, Volume 89, 2017, Pages 41-66

Abstract Interpretation with Unfoldings

Authors: Marcelo Sousa, César Rodríguez, Vijay D'Silva, Daniel Kroening

Abstract: We present and evaluate a technique for computing path-sensitive interference conditions during abstract interpretation of concurrent programs. In lieu of fixed point computation, we use prime event structures to compactly represent causal dependence and interference between sequences of transformers. Our main contribution is an unfolding algorithm that uses a new notion of independence to avoid r… ▽ More We present and evaluate a technique for computing path-sensitive interference conditions during abstract interpretation of concurrent programs. In lieu of fixed point computation, we use prime event structures to compactly represent causal dependence and interference between sequences of transformers. Our main contribution is an unfolding algorithm that uses a new notion of independence to avoid redundant transformer application, thread-local fixed points to reduce the size of the unfolding, and a novel cutoff criterion based on subsumption to guarantee termination of the analysis. Our experiments show that the abstract unfolding produces an order of magnitude fewer false alarms than a mature abstract interpreter, while being several orders of magnitude faster than solver-based tools that have the same precision. △ Less

Submitted 1 May, 2017; originally announced May 2017.

Comments: Extended version of the paper (with the same title and authors) to appear at CAV 2017

Complex Network Tools to Understand the Behavior of Criminality in Urban Areas

Authors: Gabriel Spadon, Lucas C. Scabora, Marcus V. S. Araujo, Paulo H. Oliveira, Bruno B. Machado, Elaine P. M. Sousa, Caetano Traina-Jr, Jose F. Rodrigues-Jr

Abstract: Complex networks are nowadays employed in several applications. Modeling urban street networks is one of them, and in particular to analyze criminal aspects of a city. Several research groups have focused on such application, but until now, there is a lack of a well-defined methodology for employing complex networks in a whole crime analysis process, i.e. from data preparation to a deep analysis o… ▽ More Complex networks are nowadays employed in several applications. Modeling urban street networks is one of them, and in particular to analyze criminal aspects of a city. Several research groups have focused on such application, but until now, there is a lack of a well-defined methodology for employing complex networks in a whole crime analysis process, i.e. from data preparation to a deep analysis of criminal communities. Furthermore, the "toolset" available for those works is not complete enough, also lacking techniques to maintain up-to-date, complete crime datasets and proper assessment measures. In this sense, we propose a threefold methodology for employing complex networks in the detection of highly criminal areas within a city. Our methodology comprises three tasks: (i) Map** of Urban Crimes; (ii) Criminal Community Identification; and (iii) Crime Analysis. Moreover, it provides a proper set of assessment measures for analyzing intrinsic criminality of communities, especially when considering different crime types. We show our methodology by applying it to a real crime dataset from the city of San Francisco - CA, USA. The results confirm its effectiveness to identify and analyze high criminality areas within a city. Hence, our contributions provide a basis for further developments on complex networks applied to crime analysis. △ Less

Submitted 24 December, 2016; v1 submitted 19 December, 2016; originally announced December 2016.

Comments: 7 pages, 2 figures, 14th International Conference on Information Technology : New Generations

MSC Class: 05C82; 91C20; 68R10 ACM Class: G.2.2; G.2.3; H.2.8; H.3.3; I.5

Bounded Model Checking of C++ Programs Based on the Qt Framework (extended version)

Authors: Felipe R. M. Sousa, Lucas C. Cordeiro, Eddie B. de Lima Filho

Abstract: The software development process for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, consumer electronics companies usually invest a lot of resources in fast and automatic verification processes, in order to create robust systems and reduce product recall rates. Because of that, the present paper proposes a simplifie… ▽ More The software development process for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, consumer electronics companies usually invest a lot of resources in fast and automatic verification processes, in order to create robust systems and reduce product recall rates. Because of that, the present paper proposes a simplified version of the Qt framework, which is integrated into the Efficient SMT-Based Bounded Model Checking tool to verify actual applications that use the mentioned framework. The method proposed in this paper presents a success rate of 94.45%, for the developed test suite. △ Less

Submitted 5 September, 2015; originally announced September 2015.

Comments: extended version of paper published at GCCE'15

Unfolding-based Partial Order Reduction

Authors: César Rodríguez, Marcelo Sousa, Subodh Sharma, Daniel Kroening

Abstract: Partial order reduction (POR) and net unfoldings are two alternative methods to tackle state-space explosion caused by concurrency. In this paper, we propose the combination of both approaches in an effort to combine their strengths. We first define, for an abstract execution model, unfolding semantics parameterized over an arbitrary independence relation. Based on it, our main contribution is a n… ▽ More Partial order reduction (POR) and net unfoldings are two alternative methods to tackle state-space explosion caused by concurrency. In this paper, we propose the combination of both approaches in an effort to combine their strengths. We first define, for an abstract execution model, unfolding semantics parameterized over an arbitrary independence relation. Based on it, our main contribution is a novel stateless POR algorithm that explores at most one execution per Mazurkiewicz trace, and in general, can explore exponentially fewer, thus achieving a form of super-optimality. Furthermore, our unfolding-based POR copes with non-terminating executions and incorporates state-caching. Over benchmarks with busy-waits, among others, our experiments show a dramatic reduction in the number of executions when compared to a state-of-the-art DPOR. △ Less

Submitted 3 July, 2015; originally announced July 2015.

Comments: Long version of a paper with the same title appeared on the proceedings of CONCUR 2015

ACM Class: D.2.4

Free Instrument for Movement Measure

Authors: Norberto Peña, Bruno Cecílio Credidio, Lorena Peixoto Nogueira Rodriguez Martinez Salles Corrêa, Lucas Gabriel Souza França, Marcelo do Vale Cunha, Marcos Cavalcanti de Sousa, João Paulo Bomfim Cruz Vieira, José Garcia Vivas Miranda

Abstract: This paper presents the validation of a computational tool that serves to obtain continuous measurements of moving objects. The software uses techniques of computer vision, pattern recognition and optical flow, to enable tracking of objects in videos, generating data trajectory, velocity, acceleration and angular movement. The program was applied to track a ball around a simple pendulum. The metho… ▽ More This paper presents the validation of a computational tool that serves to obtain continuous measurements of moving objects. The software uses techniques of computer vision, pattern recognition and optical flow, to enable tracking of objects in videos, generating data trajectory, velocity, acceleration and angular movement. The program was applied to track a ball around a simple pendulum. The methodology used to validate it, taking as a basis to compare the values measured by the program, as well as the theoretical values expected according to the model of a simple pendulum. The experiment is appropriate to the method because it was built within the limits of the linear harmonic oscillator and energy losses due to friction had been minimized, making it the most ideal possible. The results indicate that the tool is sensitive and accurate. Deviations of less than a millimeter to the extent of the trajectory, ensures the applicability of the software on physics, whether in research or in teaching topics. △ Less

Submitted 29 June, 2013; originally announced July 2013.

Comments: Accepted for publication at the RBEF - Revista Brasileira de Ensino de Física

Lissom, a Source Level Proof Carrying Code Platform

Authors: Joao Gomes, Daniel Martins, Simao Melo de Sousa, Jorge Sousa Pinto

Abstract: This paper introduces a proposal for a Proof Carrying Code (PCC) architecture called Lissom. Started as a challenge for final year Computing students, Lissom was thought as a mean to prove to a sceptic community, and in particular to students, that formal verification tools can be put to practice in a realistic environment, and be used to solve complex and concrete problems. The attractiveness o… ▽ More This paper introduces a proposal for a Proof Carrying Code (PCC) architecture called Lissom. Started as a challenge for final year Computing students, Lissom was thought as a mean to prove to a sceptic community, and in particular to students, that formal verification tools can be put to practice in a realistic environment, and be used to solve complex and concrete problems. The attractiveness of the problems that PCC addresses has already brought students to show interest in this project. △ Less

Submitted 15 March, 2008; originally announced March 2008.

Comments: Poster presented at the International Workshop on Proof-Carrying Code (PCC 06), 2006