Dissertation Talk: Efficient Sampling of SAT and SMT Solutions for Testing and Verification

Seminar: Dissertation Talk: CS | May 10 | 3:30-4:30 p.m. | 373 Soda Hall

 Rafael Dutra

 Electrical Engineering and Computer Sciences (EECS)

The problem of generating a large number of diverse solutions to a logical constraint has important applications in testing, verification, and synthesis for both software and hardware. The solutions generated could be used as inputs that exercise some target functionality in a program or as random stimuli to a hardware module. The sampling of solutions can be combined with techniques such as fuzz testing, symbolic execution, and constrained-random verification to uncover bugs and vulnerabilities in real programs and hardware designs. However, generating such solutions efficiently while achieving a good coverage of the constraint space is still a challenge today.

In this talk, I will present new tools we developed for efficient sampling of solutions to Boolean (SAT) and Satisfiability Modulo Theories (SMT) constraints. I will describe a novel algorithm QuickSampler that allows the generation of millions of solutions with only tens of queries to a constraint solver, being orders of magnitude faster than previous state-of-the-art samplers. I will also show that it can be extended to handle large and complex SMT formulas in SMTSampler. Finally, I will describe our new idea for coverage-guided sampling to allow shaping the distribution of solutions in a problem-specific basis.

 rtd@cs.berkeley.edu