Lucas Martinelli Tabajara

Cursou Bacharelado em Ciência da Computação na Universidade Federal do Rio Grande do Sul (UFRGS), onde também realizou pesquisa na área de computação social sob orientação do Prof. Luís Lamb. Em 2013 realizou intercâmbio na Rice University, em Houston, Texas, através do programa de graduação sanduíche Ciência Sem Fronteiras, com bolsa CAPES, onde trabalhou com o Prof. Moshe Vardi em um projeto sobre síntese de funções booleanas. Em 2015 foi admitido pelo programa de Doutorado em Ciência da Computação da Rice University, sob orientação do Prof. Vardi e com bolsa de doutorado pleno CNPq. Durante o doutorado, realizou pesquisa na área de síntese e métodos formais. Em 2017 defendeu tese de Mestrado em Ciência da Computação extendendo o trabalho de pesquisa desenvolvido durante a graduação, intitulada "BDD-Based Boolean Synthesis". Em 2021 defendeu tese de Doutorado em Ciência da Computação, intitulada "Exploring Finite-Word Automata for Reactive Synthesis", na qual apresentou e analisou algoritmos baseados em autômatos finitos para a realização de síntese reativa a partir de especificações em lógica temporal.

Studied Computer Science as an undergraduate in Universidade Federal do Rio Grande do Sul (UFRGS), where he also developed research in the field of social computing under orientation of Prof. Luís Lamb. In 2013 attended Rice University, in Houston, Texas, as a visiting student through the Brazilian Scientific Mobility Program (BSMP), sponsored by CAPES, where he collaborated with Prof. Moshe Vardi in a project on synthesis of boolean functions. In 2015 was admitted by Rice University's Computer Science Ph.D. program, under orientation of Prof. Vardi and sponsored by CNPq. In 2017 defended a Master's thesis in Computer Science extending the research work developed during undergrad, entitled "BDD-Based Boolean Synthesis". In 2021 defended a Ph.D. thesis in Computer Science, entitled "Exploring Finite-Word Automata for Reactive Synthesis", in which he presented and analyzed algorithms based on finite automata for performing reactive synthesis from temporal logic specifications.