Many computational tools have recently begun to benefit from the use of the symmetry inherent in the tasks they solve, and use general-purpose graph symmetry tools to uncover this symmetry. However, existing tools suffer quadratic runtime in the number of symmetries explicitly returned and are of limited use on very large, sparse, symmetric graphs. This paper introduces a new symmetry-discovery algorithm which exploits the sparsity present not only in the input but also the output, i.e., the symmetries themselves. By avoiding quadratic runtime on large graphs, it improves state-of- the-art runtimes from several days to less than a second.

This paper presents novel techniques for checking the soundness of a type system automatically using a software model checker. Our idea is to systematically generate every type correct intermediate program state (within some finite bounds), execute the program one step forward if possible using its small step operational semantics, and then check that the resulting intermediate program state is also type correct--but do so efficiently by detecting similarities in this search space and pruning away large portions of the search space. Thus, given only a specification of type correctness and the small step operational semantics for a language, our system automatically checks type soundness by checking that the progress and preservation theorems hold for the language (albeit for program states of at most some finite size). Our preliminary experimental results on several languages--including a language of integer and boolean expressions, a simple imperative programming language, an object-oriented language which is a subset of Java, and a language with ownership types--indicate that our approach is feasible and that our search space pruning techniques do indeed significantly reduce what is otherwise an extremely large search space. Our paper thus makes contributions both in the area of checking soundness of type systems, and in the area of reducing the state space of a software model checker.

This paper presents novel language and analysis techniques that significantly speed up software model checking of data structure properties. Consider checking a red-black tree implementation. Traditional software model checkers systematically generate all red-black tree states (within some given bounds) and check every red-black tree operation (such as insert, delete, or lookup) on every red-black tree state. Our key idea is as follows. As our checker checks a red-black tree operation o on a red-black tree state s, it uses program analysis techniques to identify other red-black tree states s'1, s'2, ..., s'k on which the operation o behaves similarly. Our analyses guarantee that if o executes correctly on s, then o will execute correctly on every s'i. Our checker therefore does not need to check o on any s'i once it checks o on s. It thus safely prunes those state transitions from its search space, while still achieving complete test coverage within the bounded domain. Our preliminary results show orders of magnitude improvement over previous approaches. We believe our techniques can make model checking significantly faster, and thus enable checking of much larger programs and complex program properties than currently possible.

Instances of the Boolean satisfiability problem (SAT) arise in many areas of circuit design and verification. These instances are typically constructed from some human-designed artifact, and thus are likely to possess much inherent symmetry and sparsity. Previous work[4] has shown that exploiting symmetries results in vastly reduced SAT solver run times, often with the search for the symmetries themselves dominating the total SAT solving time. Our contribution is twofold. First, we dissect the algorithms behind the venerable NAUTY[9] package, particularly the partition refinement procedure responsible for the majority of search space pruning as well as the majority of run time overhead. Second, we present a new symmetry-detection tool, SAUCY, which outperforms NAUTY by several orders of magnitude on the large, structured CNF formulas generated from typical EDA problems.