Hi, I’m Vinicius! 👋

Technical degree in Computer Science from CEFET-MG and currently an undergraduate student in Computer Science at UFMG. I am interested in areas such as Theoretical Computer Science, Formal Methods, and Satisfiability Modulo Theories (SMT). Currently, I work as a researcher student, implementing support for new theories in the SMT proof checker Carcara. Passionate about Linux and a number one fan of Monster by Naoki Urasawa.

Education

Universidade Federal de Minas Gerais

Bachelor’s degree in Computer Science May 2021 - Aug 2026

Centro Federal de Educação Tecnológica de Minas Gerais

Technical Course in Computer Science Feb 2017 - Dec 2019

Research

Publications

Nothing to see here yet :(

Presentations/talks

Nothing to see here yet :(

Projects and contributions

Carcara

Carcara is a proof checker and elaborator for SMT proofs in the Alethe format. It is mainly maintained by the members of the SMITE group from the Computer Science Department at UFMG.

cvc5

cvc5 is a tool for determining the satisfiability of a first order formula modulo a first order theory (or a combination of such theories). It is the fifth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3, CVC4) but does not directly incorporate code from any previous version prior to CVC4.

simple-cdcl

A simple Python implementation of the Conflict-Driven Clause Learning (CDCL) algorithm for solving SAT problems. The implementation incorporates the 2-watched literals technique and the VSIDS decision heuristic. This project was developed as part of the course Theory and Practice of SMT Solving at UFMG.

GRASP + PR heuristic for the Graph Coloring Problem

Research project focused on investigating the performance of a Greedy Randomized Adaptive Search Procedure (GRASP) heuristic with Path-Relinking applied to the Graph Coloring Problem. This project was developed as part of the course Heurísticas e Metaheurísticas at UFMG.

Work experience

Undergraduate Researcher in Formal Methods

Departamento de Ciência da Computação - UFMG Jul 2023 - present I worked on the integration of the SMT solver cvc5 with the proof checker Carcara, enabling the production and verification of proofs in the Alethe format during the solver's regression tests. I'm currently working on extending Carcara with support for new theories, using techniques from the literature, in order to enable it to verify a broader set of Alethe proofs.

Fullstack developer

Zeester Sept 2021 - Mar 2023 I contributed to the development and maintenance of a customer management dashboard, working on the frontend with ReactJS and on the backend with Node.js, both in TypeScript, within a microservices architecture integrated with MongoDB. My role included implementing new features, fixing bugs, and ensuring platform stability. I also developed a client onboarding platform with a complete payment flow, integrating secure gateways and database synchronization.

Mobile developer

Geobyte Consultoria e Tecnologia GIS Feb 2021 - Jul 2021 I developed and maintained cross-platform applications used for data collection in remote areas. Additionally, I implemented an offline-first strategy in the applications to ensure data persistence in locations without network coverage or internet access.

Fullstack developer

Comp Júnior Apr 2020 - Oct 2021 I worked as a full-stack developer on several projects during my time at Comp, with a stronger focus on back-end development. Additionally, I assisted the infrastructure team in reviewing and modernizing the deployment strategy used and was one of the organizers and content creators for an internal training program on mobile development using JavaScript, React Native, and Expo.