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

My general research interest is the interplay of symbolic computation and satisfiability checking. I am also interested in 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.