The security of the national computing infrastructure is critical for consumer confidence, protection of privacy, protection of valuable intellectual property, and even national security. Logic-based approaches to security have been gaining popularity, in part because they provide a precise way to describe and reason about the kinds of complexity found in real systems. Perhaps even more importantly, automated reasoning techniques can be used to assist users in navigating this complexity. Despite the promise of automated reasoning, its use in practical applications is still limited. One of the primary reasons for this is that for many problems, automated reasoning methods are not fast enough, especially for use in interactive environments (such as browser plug-ins in desktop computing, or mobile applications running on smart phones and PDAs). This project aims to address the performance weakness of automated reasoning by investigating novel designs and algorithms with the unifying theme of exploiting parallelism. The project will focus on three main areas of automated deduction: Boolean satisfiability, first-order reasoning, and satisfiability modulo theories.
Automated reasoning techniques are used as "engines" in many applications. They are capable in some cases of automatically answering questions like "does this program have a specific bug?" or "is it possible to exploit this software maliciously?" In many cases, however, the automated reasoning takes too long to be practical. This project aimed to address this by exploring how best to use parallelism in automated reasoning. There were two main projects. The first focused on parallelizing reasoning about Boolean satisfiability (SAT). SAT engines are used in many applications such as software modeling and circuit design and verification. We explored a technique known as Stalmarck's method which is less well-known than current best-practice techniques and is more amenable to parallelization. We implemented a parallel Stalmarck solver and showed that it was possible to get near-linear speed-up on small examples. While the overall performance was still far behind the best sequential techniques, we believe that our results are promising and suggest that more investiagion is warranted. A Stalmarck solver could at the very least be used in combination with a standard SAT solver and this could lead to significant speed-ups in some cases. The other project was to implement a parallel SMT solver. SMT solvers can reason at a higher level than Boolean solvers. They understand arithmetic and equations for example. SMT solvers are also used in many important applications. We used CVC4, a state-of-the-art SMT research platform being developed at NYU. We used a "portfolio" approach meaning that several instances of the solver are run in parallel with different configurations and the first to solve the problem terminates all of the instances. This is very course-grained parallelism but it seems to be the most effective approach so far. Some sharing of information in the form of "learned lemmas" is possible between the different instances. We found that the sharing of information was typically not helpful for SMT problems, but this could be because our sharing mechanism was fairly primitive. However, the portfolio approach does work well on many problems because SMT (like SAT) is very sensitive to configuration options. So, by running several different configurations in parallel, it is likely that performance gains will be realized. CVC4 (with these parallelization options) is publicly available at http://cvc4.cs.nyu.edu. An open question that we did not explore is whether more fine-grained parallelism (i.e. at the theory level or lower) would significantly improve the performance of typical SMT queries.
