Rafael Tupynambá Dutra

Rafael Tupynambá Dutra

Ph.D. Candidate in Computer Science advised by Koushik Sen.


Ph.D. in Computer Science, UC Berkeley 2019
Dissertation Talk
Efficient Sampling of SAT and SMT Solutions for Testing and Verification
Advisor: Koushik Sen

Master in Mathematics, UFMG 2014
Dissertation Talk
Riemann's “non-differentiable” function
Advisor: Márcio Soares

Bachelor in Automation and Control Engineering, UFMG 2014
Final Project Talk
Development of Embedded Software for an Unmanned Aerial Vehicle
Advisor: Leonardo Tôrres


QuickSampler and SMTSampler are techniques for sampling millions of solutions to a SAT formula or SMT formula. They are orders of magnitude faster than previous techniques and allow the generation of a diverse set of solutions.

QuickSampler and SMTSampler work by computing patterns of bit flips that preserve the satisfiability of the formula. By combining those bit flip patterns, they can generate millions of solutions for complex constraints in minutes.

GuidedSampler is an extension of SMTSampler that allows guiding the distribution of solutions based on a coverage points specified by the user. GuidedSampler can efficiently generate solutions that cover a large number of diverse coverage classes.

Coverage classes

FMCAD 2019 paper Talk
GuidedSampler: Coverage-guided Sampling of SMT Solutions
Rafael Dutra, Jonathan Bachrach, Koushik Sen

SMTSampler algorithm

ICCAD 2018 paper Talk
SMTSampler: Efficient Stimulus Generation from Complex SMT Constraints
Rafael Dutra, Jonathan Bachrach, Koushik Sen

Unique solutions generatedDistribution of solutions generated

ICSE 2018 paper Talk
Efficient Sampling of SAT Solutions for Testing
Rafael Dutra, Kevin Laeufer, Jonathan Bachrach, Koushik Sen


Instructor for CS 161 - Computer Security for Summer 2019.

GSI for CS 161 - Computer Security for Fall 2018 and Spring 2019.