I am a professor of the Federal Institute of Education, Science and Technology of Espírito Santo at Campus Serra. I teach mainly courses related to logic, discrete mathematics, theory of computation, functional programming, and data science. I earned my Doctoral degree in Education at the Universidad del Norte, and my Master in Informatics, and Computer Engineer degrees at the Universidade Federal do Espírito Santo.
I am also a member of the Techniques and Theory of Computation Research Group, Nu[TeC]². I am very passionate about computer science and have a wide range of interests, including functional and logic programming, formal methods, formal verification, artificial intelligence (both modern and classical methods), and data science. I also have a strong interest in education, especially in mathematics and computer science education at the high education level, and the use of games and gamification in education.
Ph.D. in Education, 2013
Universidad del Norte
M.Sc. in Informatics, 2001
Federal University of Espírito Santo
B.Eng. in Computer Engineering, 1995
Federal University of Espírito Santo
One of the responsibilities of higher education institutions in Brazil is to track the professional progress of their alumni. This project aims to automate this task by monitoring students' activity in social networks.
Proposes to apply state of the art in artificial intelligence to extract and aggregate knowledge about technological information to inform the generation of a technical standard for licensing the industrial processes of handling and storage of post-processed ornamental rocks.
Aims to apply formal methods of software engineering and software verification to produce a reliable software platform for flight control of unmanned aerial vehicles.
This project aims to take advantage of sensor data and machine learning algorithms to predict and prevent breakout problems study of continuous casting steel.
One possible approach to address the performance issues of large scale identification systems is to use light biometric measures to reduce the search space in a first step and apply strong biometric measures in a second identification step. This project aims to investigate this approach.
Aims to develop a mobile solution to identify and map the observations of sea turtle species that occur on the Brazilian coast, using machine learning algorithms for image recognition.
Development of a mobile app to assist people with dysphemia to practice the diction of selected words and improve life quality and self-confidence.
An active price monitor for web stores, assisting customers to compare products and prices.
NÊMESIS sought to develop a reference model for information, communication, and biometric technologies for technical and scientific police. The project is developed in cooperation with the Technical Police Secretariat of the State of Espírito Santo.
Formal logic plays a fundamental role in computer science. Unfortunately, it is observed that the effectiveness of the learning process of formal logic has proved to be less than ideal. This work presents the ∃lementar system; a system that integrates a proof assistant in a gamified context, i.e., that uses game elements to promote student’s engagement and motivation. After introducing ∃lementar’s main features, this work presents preliminary data that point to an improvement in student’s performance indicators.
Formal logic plays a fundamental role in computer science. It is necessary to introduce the fundamentals of this discipline so that these students can achieve mastery across the range of its applications in computer science. Unfortunately, it is observed that the efficiency of the learning process the Bachelor in Information Systems program, has proved to be less than ideal. In this work, we propose that it is possible to increase the effectiveness of the learning process through the use of proof assistants as a teaching tool, but with the introduction of game-like elements. This approach has been known as gamification. We present an overview of the theoretical basis that supports the use of gamification, we then proceed to describe a proposal of a gamified system for learning formal logic, as well as a prototype implementation of this proposed system. We conclude this paper presenting some results of an experiment conducted by adopting our prototype as a learning tool during one academic semester. We then compare these results with the previous semester and analyze the possibilities of the use of gamification in an educational setting.
Multi-valued Model Checking extends classical, two-valued model checking to multi-valued logic such as Quasi-Boolean logic. The added expressivity is useful in dealing with such concepts as incompleteness and uncertainty in target systems, while it comes with the cost of time and space. Chechik and others proposed an efficient reduction from multi-valued model checking problems to two-valued ones, but to the authors' knowledge, no study was done for multi-valued bounded model checking. In this paper, we propose a novel, efficient algorithm for multi-valued bounded model checking. A notable feature of our algorithm is that it is not based on reduction of multi-values into two-values; instead, it generates a single formula which represents multi-valuedness by a suitable encoding, and asks a standard SAT solver to check its satisfiability. Our experimental results show a significant improvement in the number of variables and clauses and also in execution time compared with the reduction-based one.
Multi-valued Model Checking is an extension of classical, two-valued model checking with multi-valued logic. Multi-valuedness has been proved useful in expressing additional information such as incompleteness, uncertainty, and many others, but with the cost of time and space complexity. This paper addresses this problem, and proposes a new algorithm for Multi-valued Model Checking. While Chechik et al. have extended BDD-based Symbolic Model Checking algorithm to the multi-valued case, our algorithm extends Bounded Model Checking (BMC), which can generate a counterexample of minimum length efficiently (if any). A notable feature of our algorithm is that it directly generates conjunctive normal forms, and never reduces multi-valued formulas into many slices of two-valued formulas. To achieve this feature, we extend the BMC algorithm to the multi-valued case and also devise a new translation of multi-valued propositional formulas. Finally, we show experimental results and compare the performance of our algorithm with that of a reduction-based algorithm.