ABSTRACT. Algorithms have transformed every aspect of society, including communication, transportation, commerce, finance, and health. The revolution enabled by computing has been extraordinarily valuable. The largest tech companies generate a trillion dollars a year and employ 1 million people. But technology does not affect everyone in the same way. In this talk, we will examine how new technologies affect marginalized communities and think about what technology and academic research would look like if its goal was to serve the disenfranchised.

ABSTRACT. While static symmetry breaking has been explored in the SAT community for decades, only as of 2010 research has focused on exploiting the same discovered symmetry dynamically, during the run of the SAT solver, by learning extra clauses. The two methods are distinct and not compatible. The former prunes solutions, whereas the latter does not -- it only prunes areas of the search that do not have solutions, like standard conflict clauses. Both approaches, however, require what we call \emph{full symmetry}, namely a propositionally-consistent mapping $\sigma$ between the literals, such that $\sigma(\varphi) \equiv \varphi$, where here $\equiv$ means syntactic equivalence modulo clause ordering and literal ordering within the clauses. In this article we show that such full symmetry is not a necessary condition for adding extra clauses: isomorphism between possibly-overlapping subgraphs of the colored incidence graph is sufficient. While finding such subgraphs is a computationally hard problem, there are many cases in which they can be detected a priory by analyzing the high-level structure of the problem from which the CNF was derived. We demonstrate this principle with several well-known problems that recently received attention in the literature.

ABSTRACT. In many areas of computer science, we are given an unsatisfiable formula F in CNF, i.e., a set of clauses, with the goal to analyze the unsatisfiability. A kind of such analysis is to identify Minimal Correction Subsets (MCSes) of F, i.e., minimal subsets of clauses that need to be removed from F to make it satisfiable. Equivalently, one might identify the complements of MCSes, i.e., Maximal Satisfiable Subsets (MSSes) of F. The more MSSes (MCSes) of F is identified, the better insight into the unsatisfiability can be obtained. Hence, there were proposed many algorithms for complete MSS (MCS) enumeration. Unfortunately, the number of MSSes can be exponential w.r.t. |F|, which often makes the complete enumeration practically intractable.

In this work, we attempt to cope with the intractability of complete MSS enumeration by initiating the study on MSS decomposition. In particular, we propose several techniques that often allow for decomposing the input formula F into several subformulas. Subsequently, we explicitly enumerate all MSSes of the subformulas, and then combine those MSSes to form MSSes of the original formula F. An extensive empirical study demonstrates that due to the MSS decomposition, the number of MSSes that need to be explicitly identified is often exponentially smaller than the total number of MSSes. Consequently, we can improve upon a scalability of contemporary MSS enumeration approaches by many orders of magnitude.

ABSTRACT. Given a formula F, the problem of uniform sampling seeks to sample solutions of F uniformly at random. Uniform sampling is a fundamental problem with a wide variety of applications. The computational intractability of uniform sampling has led to the development of several samplers that are heuristics and are not accompanied by theoretical analysis of their distribution. Recently, Chakraborty and Meel (2019) designed the first scalable sampling tester, Barbarik, based on a grey-box sampling technique for testing if the distribution, according to which the given sampler is sampling, is close to the uniform or far from uniform. While the theoretical analysis of Barbarik provides only unconditional soundness guarantees, the empirical evaluation of Barbarik did show its success in determining that some of the off-the-shelf samplers were far from a uniform sampler.

The availability of Barbarik has the potential to spur the development of samplers and testing techniques such that developers can design sampling methods that can be accepted by Barbarik even though these samplers may not be amenable to a detailed mathematical analysis. In this paper, we present the realization of this aforementioned promise. Based on the flexibility offered by CryptoMiniSat, we design a sampler CMSGen that promises the achievement of the sweet spot of the quality of distributions and runtime performance. In particular, CMSGen achieves significant runtime performance improvement over the existing samplers. We conduct two case studies, and demonstrate that the usage of CMSGen leads to significant runtime improvements in the context of combinatorial testing and functional synthesis.

A salient strength of our work is the simplicity of CMSGen, which stands in contrast to complicated algorithmic schemes developed in the past that fail to attain the desired quality of distributions with practical runtime performance.

ABSTRACT. Optimized SAT solvers not only preprocess the clause set, they also transform it during solving as inprocessing. Some preprocessing techniques have been generalized to first-order logic with equality. In this paper, we port inprocessing techniques to work with superposition, and we strengthen preprocessing. Specifically, we look into elimination of hidden literals, variables (predicates), and blocked clauses. Our evaluation using the Zipperposition prover confirms that the new techniques usefully supplement the existing superposition machinery.

ABSTRACT. In recent years, cloud service providers have sold computation in increasingly granular units. Most recently, “serverless” executors run a single executable with restricted network access and for a limited time. The benefit of these restrictions is scale: thousandway parallelism can be allocated in seconds, and CPU time is billed with subsecond granularity. To exploit these executors, we introduce gg-SAT: an implementation of divide-and-conquer SAT solving. Infrastructurally, gg-SAT departs substantially from previous implementations: rather than handling process or server management itself, gg-SAT builds on the gg framework, allowing computations to be executed on a configurable backend, including serverless offerings such as AWS Lambda. Our experiments show that when run on the same hardware, gg-SAT performs competitively with other D&C solvers, and that the 1000-way parallelism it offers (through AWS Lambda) is useful for some challenging SAT instances.

ABSTRACT. Deep Neural Networks (DNNs) play an increasingly important role in various computer systems. In order to create these networks, an engineer specifies a desired topology, and an automated training algorithm then selects the network's weights. The selection of topology remains a form of art, and can often result in networks that are unnecessarily large --- and consequently are incompatible with and devices that have limited memory, battery or computational power. Here, we propose to address this challenge by harnessing recent advances in neural network verification. We present a framework and methodologies for discovering redundancies in DNNs --- specifically, for finding redundant neurons, which can then be removed. By using sound verification techniques, we can formally guarantee that our simplified network is equivalent to the original. We also show how to combine our technique with slicing, which results in a family of small DNNs that are together equivalent to the original. The DNNs produced by our approach are significantly smaller, can be deployed on additional systems, and are even more amenable to formal verification of additional properties. We implement our approach in a freely available tool, and evaluate it on a variety of real-world DNNs.

ABSTRACT. Deep neural networks (DNNs) have gained significant popularity in recent years, becoming the state of the art in a variety of domains. In particular, deep reinforcement learning (DRL) has recently been employed to train DNNs that act as control policies for various types of real-world systems. In this work, we present the whiRL 2.0 tool, which implements a new approach for verifying complex properties of interest for such DRL systems. To demonstrate the benefits of whiRL 2.0, we apply it to case studies from the communication networks domain that have recently been used to motivate formal verification of DRL systems, and which exhibit characteristics that are conducive for scalable verification. We propose techniques for performing k-induction and automated invariant inference on such systems, and use these techniques for proving safety and liveness properties of interest that were previously impossible to verify due to the scalability barriers of prior approaches. Furthermore, we show how our proposed techniques provide insights into the inner workings and the generalizability of DRL systems. whiRL 2.0 is publicly available online.

ABSTRACT. We present a new approach for exploring and synthesizing interpretations that explain the behavior of black-box machine learning models. Constructing human-understandable interpretations often requires balancing conflicting objectives. A simple interpretation may be easier to understand for humans while being less precise in its predictions vis-a-vis a complex interpretation. Existing methods for synthesizing interpretations use a single objective function and are optimized for a single class of interpretations. In contrast, we provide a more general and multi-objective synthesis framework that allows users to choose (1) the class of syntactic templates from which an interpretation should be synthesized, and (2) quantitative measures on both the correctness and explainability of an interpretation. For a given black-box, our approach allows users to explore the space of Pareto-optimal interpretations with respect to the correctness and explainability measures. We show that the underlying multi-objective interpretation synthesis problem can be solved via a reduction to quantitative constraint solving, such as weighted maximum satisfiability. To demonstrate the flexibility of our approach we have applied it for the synthesis of interpretations for black-box neural-network classifiers. Our experiments show that there often exists a rich and varied set of choices for interpretations that are missed by existing approaches.

ABSTRACT. Stateless model checking (SMC) coupled with dynamic partial order reduction (DPOR) is an effective way for automatically verifying safety properties of loop-free concurrent programs. By design, however, SMC does not work well for programs with loops, as it cannot distinguish loop iterations that make progress from ones that revisit the same state. This results in redundant exploration that dominates the verification time.

We present SAVer (Spinloop-Aware Verifier), an SMC/DPOR extension that detects zero-net-effect spinloops and avoids redundant explorations that lead to the same local state. As confirmed by our experiments, SAVer achieves an exponential reduction in verification time and outperforms state-of-the-art tools in a variety of real-world benchmarks.

ABSTRACT. Robustness of a concurrent program ensures that its behaviors on a weak concurrency model are indistinguishable from those on a stronger model. Enforcing robustness is particularly useful when porting or migrating applications between architectures. Existing tools mostly focus on ensuring sequential consistency (SC) robustness which is a stronger condition and may result in unnecessary fences.

To address this gap, we analyze and enforce robustness between weak memory models, more specifically for two main- stream architectures: x86 and ARM (versions 7 and 8). We iden- tify robustness conditions and develop analysis techniques that facilitate porting an application between these architectures. To the best of our knowledge, this is the first approach that addresses robustness between the hardware weak memory models.

We implement our robustness checking and enforcement procedure as a compiler pass in LLVM and experiment on a number of standard concurrent benchmarks. In almost all cases, our procedure terminates instantaneously and insert significantly less fences than the naive schemes that enforce SC-robustness.