Hi! I am Pedro Saccomani, a first year PhD student at Universidade Federal de Minas Gerais, working under Haniel Barbosa supervision.

My general research interest is the interplay of symbolic computation and satisfiability checking. Currently, I am working on the production of proof certificates of Satisfiability Modulo Theories (SMT) procedures based on computer algebra.

Specifically, I am working towards a proof producing SMT theory of finite fields. I am also interested in proof generation for the theory of non-linear real arithmetic.