Bounded-exhaustive test case generators are important bug-finding tools, epitomized with tools like Korat, UDITA, and SciFe. All such tools are practically limited by scale; a given testing problem may be too large to generate all tests within reasonable time, or prohibitive amounts of memory may be required for this generation. The tools themselves may have lengthy implementations which hide their own bugs, or they may require users to familiarize themselves with many operations. In this paper, we strive to push the boundaries of what test case generators can scale to, while preserving a simple implementation and user interface. To this end, we introduce a novel programming abstraction: Memoized Monadic Iterators (MiMIs). MiMIs combine the disparate ideas of ASTGen's iterators, LogicT's additive monad interface, and SciFe's memoization into a single coherent programming abstraction. Our evaluation shows that MiMIs are typically faster than the state of the art with orders of magnitude less memory used, and that MiMIs overall scale better to big testing problems than any competitor. Thanks to their fundamental design, MiMIs are implemented in under 200 LOC (compared to thousands with most competitors), and require users to familiarize themselves with collectively only 7 operations and types (less than half as many as the state of the art), all without sacrificing generator conciseness.

Fuzzers are important bug-finding tools in both academia and industry. To ensure scientific progress, we need a metric for fuzzer comparison. Bug-based metrics are impractical because (1) the definition of "bug" is vague, and (2) mapping bug-revealing inputs to bugs requires extensive domain knowledge.In this paper, we propose an automated method for comparing fuzzers that alleviates these problems. We replace the question "What bugs can this fuzzer find?" with "What changes in program behavior over time can this fuzzer detect?". Intuitively, fuzzers which find more behavioral changes are likely to find more bugs. However, unlike bugs, behavioral changes are well-defined and readily detectable. Our evaluation, executed on three targets with several fuzzers, shows that our method is consistent with bug-based metrics, but without associated difficulties. While further evaluation is needed to establish superiority, our results show that our method warrants further investigation.

Recently, symbolic program analysis techniques have been extended to quantitative analyses using model counting constraint solvers. Given a constraint and a bound, a model counting constraint solver computes the number of solutions for the constraint within the bound. We present a parameterized model counting constraint solver for string and numeric constraints. We first construct a multi-track deterministic finite state automaton that accepts all solutions to the given constraint. We limit the numeric constraints to linear integer arithmetic, and for non-regular string constraints we over-approximate the solution set. Counting the number of accepting paths in the generated automaton solves the model counting problem. Our approach is parameterized in the sense that, we do not assume a finite domain size during automata construction, resulting in a potentially infinite set of solutions, and our model counting approach works for arbitrarily large bounds. We experimentally demonstrate the effectiveness of our approach on a large set of string and numeric constraints extracted from software applications. We experimentally compare our tool to five existing model counting constraint solvers for string and numeric constraints and demonstrate that our tool is as efficient and as or more precise than other solvers. Moreover, our tool can handle mixed constraints with string and integer variables that no other tool can.