Hi! I am Pedro Saccomani, a second 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. I am also on computer computer algebra techniques for the SMT theory of bit-vectors.

I recently worked on proof production and verified checking for the SMT theory of finite fields. Currently, I am exploring proof generation for the theory of non-linear real arithmetic and alternatives to bit-blasting to handle bit-vector arithmetic.