Search

The rise of automated systems and sensor networksin virtually all areas of industry and social life means many technologies produce streams of events rich with information. These technologies demand algorithms for evaluating queries on streams, coordinating systems that communicate with events, and monitoring streams with respect to specified constraints. In monitoring, constraints that define correct behavior, e.g., business goals, legal requirements, resource limitations, or safety and security concerns are specified in a formal language; then, an event stream is analyzed at runtime to determine if the constraints are satisfied or violated. To make monitoring effective, it is important to detect constraint violations at the earliest possible time, which we call the early violation detection problem. We study early violation detection for a class of constraints called rulesthat restrict time gaps between events and compare events' data contents. We show that (1) the general problem of early violation detection for an arbitrary set of rules is unsolvable and (2) early violation detection is possible for various subclasses of rules. For (1), we show early violation detection is closely related to the problem of finite satisfiability (whether or not a given set of rules can be satisfied by a finite event stream) and prove that finite satisfiability for a set of rules is undecidable with a reduction from the empty-tape Turing machine halting problem, which implies that early violation detection is unsolvable in general. For (2), we study restricted classes of rules. A recent proof of Kamp's Theorem provides a translation algorithm for ``dataless'' rules through translation to linear temporal logic. yielding formulas hyper-exponential in the size of the input rule. We present translation algorithms for two subclasses of dataless rules, improving the output size from hyper-exponential to single- and double-exponential, respectively. For rules with data, we first present a technique that calculates deadlines from time gaps between events, then use deadlines for early violation detection for individual rules. We extend these algorithms to monitor an acyclic set of rules by applying a chase process and satisfiability testing. We also report the performance of an implementation of these algorithms. Finally, we consider acyclic sets of rules with aggregation functions over time windows, combining the chase and satisfiability techniques with an encoding of aggregation functions in Presburger arithmetic.

Code tracing is fundamental to students’ understanding of a program, and symbolic reasoning that entails learning to use assertions with abstract input and output values, as opposed to concrete values, enhances that understanding. Symbolic reasoning teaches students valuable abstraction and logic skills that will serve them well in all aspects of programming and their softwaredevelopment careers.We use lessons integrated into an online educational tool to supplement classroom instruction to help students learn symbolic reasoning. We explore two ways for students to learn about assertions: Writing assertions to capture the behavior of given code and solving Parsons-style problems in which statements are composed to produce behavior specified in assertions. A subsequent assessment tests students’ ability to select multiple assertions given code and to select the appropriate code fragment for given assertions.The same experiment was conducted with two different populations: a large public R1 research institution and a public R2 Hispanic-Serving Institution (HSI). Overall the impacts were more pronounced at the larger institution with a bigger sample size. Students’ assessment scores showed that they could reason symbolically at both institutions. They did better at Parsons-style problems of matching code to assertions at both institutions, though the difference varied by code type. The two populations had different trends in their performance for conditional code questions as they were asked to select from among increasingly formal assertions. Students from the R1 institution had a strong downward trend, while students from the HSI maintained or slightly increased their performance. The analysis also yielded insight into student misconceptions and suggested directions for further research.

Abstract: Boolean Satisfiability (SAT) is a well-known NP-complete problem. Despite the theoretical hardness of SAT, backtracking search based Conflict Directed ClauseLearning (CDCL) SAT solvers can solve very large real-world SAT instances with surprising efficiency. The high efficiency of CDCL SAT solving is due to the careful integration of its key ingredients: preprocessing, inprocessing, decision heuristics,learning of clauses from conflicts, intelligent backtracking, and restarts.Clause learning from conflicts helps a CDCL solver to prune its search space and achieve solving efficiency. Since finding conflicts is the only way to learn clauses, generating conflicts at a high rate is crucial for CDCL SAT solving. A key component of CDCL SAT is the decision step, which heuristically selects an unassgined variable to make a boolean assignment during the search. Standard CDCL heuristics for branching are designed based on a look-back principle that uses information of past search states. Examples are Variable State Independent Decaying Sum (VSIDS) and Learning Rate Based (LRB). Both of these heuristics are conflict guided and prioritize selection of variables that are likely to lead to the discovery of conflicts.These decision heuristics play a crucial role for CDCL. However, there is a lack of empirical understanding of how these branching heuristics work. This has been regarded as an important open problem in SAT research. In this thesis, we study state-of-the-art CDCL decision heuristics empirically and design extensions of these heuristics based on the insights obtained from our empirical studies. First, we present a study on two types of decision variables: glue and no-glue variables. These are named depending on their appearance in a special type of learned clause calledglue-clause. We demonstrate that decisions with glue variables are more conflict efficient than decisions with non-glue variables. Based on this insight, we develop a decision strategy named glue bump, which prioritizes selection of glue-variables. We show that the glue bumping strategy implemented on top of state-of-the-art CDCL SAT solvers improves the performance of these solvers. Secondly, we present a study of the conflict generation patterns in CDCL with two leading CDCL branching heuristics. We discovered that con-flicts in CDCL are generated in phases of short bursts, often followed by longer conflict depression phases, where the search does not find any conflicts for a number of consecutive decisions. We developed a CDCL algorithmic extension named expAT that performs random exploration during substantial conflict depression phases. We demonstrated that expSAT improves the performance of state-of-the-art CDCL SAT solvers on two years of SAT competition benchmarks and on a set of hard cryptographic instances from Bitcoin mining benchmarks. Thirdly, we study conflict producing decisions in CDCL, where we distinguish two types of decisions: single conflict (sc) and multi-conflict (mc) decisions. We present a characterization of sc and mc decisions, based on the quality of learned clauses that each produces. With this characterization, we propose a decision strategy named Common ReasonVariable score Reduction (CRVR). CRVR de-prioritizes selection of those variables,which contribute to the generation of lower quality learned clauses in poor decisions. Our empirical evaluation of CRVR demonstrates performance improvement of state-of-the-art CDCL SAT solvers on Satisfiable instances.

Modular verification of parallel and concurrent software built from reusable data abstractions is a challenging problem. Reasoning about sequential software can be modularized using the specifications of data abstractions, but the need to consider implementation details complicates reasoning about parallel execution.Addressing this challenge requires advancing the state of the art in several ways, beginning with a theoretical foundation. The A/P Calculus for describing the effects of program actions is developed in this dissertation to enable sound modular reasoning about parallel programs with non-interfering parallel sections of operation calls on abstract data types. Building on the calculus and a programming language with clean semantics, a methodology for designing decomposable data abstractions is presented to produce fork-join parallel programs that are manifestly data race free and readily amenable to modular reasoning. A new specification construct, the non-interference contract, is proposed to enhance the specification of data abstractions to hide implementation details and yet facilitate modular reasoning about parallel programs that share objects among processes.As a key first step to transition these results to practice, this dissertation describes Clean++, a discipline for writing software in C++ that leverages move semantics to make ownership transfer the primary data movement operation (as opposed to either deep or shallow copying) and produce programs that are amenable to formal verification with only minimal scaffolding related to pointer manipulation.

Many RDF systems support reasoning with Datalog rules via materialisation, where all conclusions of RDF data and the rules are precomputed and explicitly stored in a preprocessing step. As the amount of RDF data used in applications keeps increasing, processing large datasets often requires distributing the data in a cluster of shared-nothing servers. Whereas numerous distributed query answering techniques are known, distributed materialisation is less well understood. In this paper, we present several techniques that facilitate scalable materialisation in distributed RDF systems. First, we present a new distributed materialisation algorithm that aims to minimise communication and synchronisation in the cluster. Second, we present two new algorithms for partitioning RDF data, both of which aim to produce tightly connected partitions, but without loading complete datasets into memory. We evaluate our materialisation algorithm against two state-of-the- art distributed Datalog systems and show that our technique offers competitive performance, particularly when the rules are complex. Moreover, we analyse in depth the effects of data partitioning on reasoning performance and show that our techniques offer performance comparable or superior to the state of the art min-cut partitioning, but computing the partitions requires considerably fewer resources.

Graphical models provide a unified framework for modeling and reasoning about complex tasks. Example tasks include probabilistic inference and sequential decision making under uncertainty. Influence diagrams extend Bayesian networks with decision variables and utility functions to model the interaction between an agent and a system aiming to capture the agent's preferences. The standard task is to compute the maximum expected utility (MEU) over the influence diagram and a corresponding maximizing sequence of policies. However, finding the MEU is intractable, and it is one of the most challenging tasks in graphical models. Therefore, the goal of this dissertation is the development of decomposition bounds for influence diagrams. Computing upper bounds on the MEU is desirable also because upper bounds can facilitate anytime-solutions by acting as heuristics to guide search or sampling-based methods. Most earlier approaches for upper bounding the MEU relied on polynomial reductions to other standard tasks in graphical models. However, such reductions are ineffective in practice since they highly inflate the problem size that needs to be solved. In this dissertation, we present two direct bounding methods for IDs. The first builds on the algebraic framework for influence diagrams, called valuation algebra. Using this framework, we extend two earlier decomposition bounds to the MEU task. The second method provides upper bounds by exploiting an exponentiated utility form of the MEU which can be bounded by a conventional task (i.e., marginal MAP) over a standard probabilistic graphical model. This enables the use of two variational decomposition bounds for the well known marginal MAP task, yielding what we call exponentiated utility bounds for the MEU. For both cases (using valuation algebra and using exponentiated utilities), we present two kinds of message passing algorithms derived from bounding schemes on the marginal MAP task. One is the generalized dual decomposition algorithm, which propagates messages over a join-graph decomposition of an ID. The other is a weighted mini-bucket algorithm that propagates messages over the mini-bucket tree decomposition. We evaluated all the algorithms empirically and compared them against earlier approaches over four synthetic benchmark domains. The empirical evaluation results show that our direct bounding schemes generate upper bounds that are orders of magnitude tighter than previous methods. In addition, the exponentiated schemes turn out to be, overall, far more effective. We also evaluated our algorithms on the well-known system administration domain and observed that one of the exponentiated algorithms exhibited a remarkable performance generating upper bounds that are within a factor of two from the exact MEU.

Formal proofs, interactively developed and machine-checked, are a means to achieve the highest level of assurance in the correctness of software. In larger verification projects, with multi-year timelines and hundreds of thousands of lines of proof text, the emerging discipline of proof engineering plays a critical role in minimizing both the cost and effort of developing formal proofs. The work presented in this thesis targets the scalability challenges present in such projects. In a systematic analysis of several large software verification projects in the interactive proof assistant Isabelle, we demonstrate that in these projects, as the size of a formal specification increases, the required effort for its corresponding proof grows quadratically. Proof engineering encompasses both authoring proofs, and developing the necessary infrastructure to make those proofs tractable, scalable and robust against specification changes. Proof automation plays a key role here. However, in the context of Isabelle, many advanced features, such as developing custom automated reasoning procedures, are outside the standard repertoire of the majority of proof authors. To address this problem, we present Eisbach: an extension to Isabelle's formal proof document language Isar. Eisbach allows proof authors to write automated reasoning procedures, known as proof methods, at the familiar level of abstraction provided by Isar. Additionally, Eisbach is extensible through specialized methods that act as general language constructs, providing high-level access to advanced features of Isabelle, such as subgoal matching. We show how Eisbach provides a framework for extending Isar with more automation than was previously possible, by allowing proof methods to be treated as first-class language elements. Today, Eisbach is already used in many Isabelle proof developments. We further demonstrate its effectiveness by implementing several language extensions, together with a collection of proof methods for performing program refinement proofs. By applying these to proofs from the L4.verified project, the one of the largest formal proof projects in history, we show that effective use of Eisbach results in a reduction in the overall proof size and required effort for a given specification.

When making decisions under uncertainty, the optimal choices are often difficult to discern, especially if not enough information has been gathered. Two key questions in this regard relate to whether one should stop the information gathering process and commit to a decision (stopping criterion), and if not, what information to gather next (selection criterion). The proposed thesis is concerned with addressing this problem in light of a new advance, known as the Same--Decision Probability (SDP), which is the probability that we would make the same decision had we known what we currently do not know. In this thesis, we show how the SDP can be used to be an effective stopping criterion, and compare it to traditional criteria to demonstrate how it provides a fresh perspective in decision making under uncertainty. Additionally, we develop the first exact algorithm to compute the SDP so that it may be used as a stopping criterion. We demonstrate the effectiveness of these algorithms on real and synthetic networks, and show that our proposed stopping criterion can lead to an early stopping of information gathering. Furthermore, we demonstrate that the SDP can be used as a selection criterion. In particular, since there are many criteria for measuring the value of information, each based on optimizing different objectives, we propose a new SDP-based criterion for measuring the value of information --- this criterion values information that leads to robust decisions (i.e., ones that are unlikely to change due to new information). We develop the first algorithm to optimize the value of information, given the SDP as the reward criterion, and show empirical results that prove the utility of this novel criterion. We further answer several questions regarding the computational complexity of the SDP, which is known to be PP^PP-complete. Finally, we present results of applying the SDP as an information gathering criterion in practical problems including tutoring systems (do we need to ask more questions?) and machine learning (do we have enough data?).

Security bugs in network-based applications allow an attacker to compromise a system from the network. Existing techniques to find bugs in network-based applications are limited because the rules by which a program interacts with its network environment (i.e., the protocol) are often unknown. Further, the complexity of stateful interactions in such applications makes bug-finding difficult.In this thesis, we explore two directions towards solving the problem of finding bugs in network-based applications. First, to overcome the problem of not knowing how an application interacts with its network environment, we propose new techniques to automatically infer the protocol model implemented by an application, and use the inferred model to guide the search for bugs. We apply our technique to infer the command-and-control protocol model of a major spam botnet, and analyze it to discover its weakest link and protocol logic flaws. The analysis leads to new ways to disable botnets and new ways to fight spam.Second, we propose new techniques to analyze programs to find bugs. Our techniques are based on a family of techniques called symbolic analysis, that are equivalent to testing with entire classes of test case inputs. We show that a synergistic combination of model inference and symbolic analysis is more effective than symbolic analysis alone. Our technique finds several new vulnerabilities in popular applications that have remained undetected for years.Symbolic analysis has limited scalability on programs of significant sizes. We propose a compositional approach to symbolic analysis, that scales to programs in the order of hundreds of thousands of lines of code (100 KLOC). Our technique uses a novel combination of satisfying assignments and proofs of unsatisfiability in a solver to generalize preconditions that must lead to bugs. Using the preconditions with the data-flow of the program allows it to prune irrelevant code from analysis. Our technique outperforms existing tools, and finds multiple new vulnerabilities in critical Internet infrastructure software.

Biologists use ontologies as a method to organize and publish their acquired knowledge. Computer scientists have shown the value of ontologies as a means for knowledge discovery. This dissertation makes a number of contributions to enable systematic biologists to better leverage their ontologies in their research. Systematic biology, or phylogenetics, is the study of evolution. “Assembling a Tree of Life” (AToL) is an NSF grand challenge to describe all life on Earth and estimate its evolutionary history. AToL projects commonly include a study a taxon (organism) to create an ontology to capture its anatomy. Such anatomy ontologies are manually curated based on the data from morphology-based phylogenetic studies. Annotated digital imagery, morphological characters and phylogenetic (evolutionary) trees are the key components of morphological studies. Given the scale of AToL, building an anatomy ontology for each taxon manually is infeasible. The primary contribution of this dissertation is automatic inference and concomitant formalization required to compute anatomy ontologies. New anatomy ontologies are formed by applying transformations on an existing anatomy ontology for a model organism. The conditions for the transformations are derived from observational data recorded as morphological characters. We automatically created the Cypriniformes Gill and Hyoid Arches Ontology using the morphological character data provided by the Cypriniformes Tree of Life (CTOL) project. The method is based on representing all components of a phylogenetic study as an ontology using a domain meta-model. For this purpose we developed Morphster, a domain-specific knowledge acquisition tool for biologists. Digital images often serve as proxies for natural specimens and are the basis of many observations. A key problem for Morphster is the treatment of images in conjunction with ontologies. We contributed a formal system for integrating images with ontologies where images either capture observations of nature or scientific hypotheses. Our framework for image-ontology integration provides opportunities for building workflows that allow biologists to synthesize and align ontologies. Biologists building ontologies often had to choose between two ontology systems: Open Biomedical Ontologies (OBO) or the Semantic Web. It was critical to bridge the gap between the two systems to leverage biological ontologies for inference. We created a methodology and a lossless round-trip mapping for OBO ontologies to the Semantic Web. Using the Semantic Web as a guide to organize OBO, we developed a mapping system which is now a community standard.

Programs have precise semantics, so we can use mathematical proof to establish their properties. These proofs are often too large to validate with the usual "social process" of mathematics, so instead we create and check them with theorem-proving software. This software must be advanced enough to make the proof process tractable, but this very sophistication casts doubt upon the whole enterprise: who verifies the verifier? We begin with a simple proof checker, Level 1, that only accepts proofs composed of the most primitive steps, like Instantiation and Cut. This program is so straightforward the ordinary, social process can establish its soundness and the consistency of the logical theory it implements (so we know theorems are "always true"). Next, we develop a series of increasingly capable proof checkers, Level 2, Level 3, etc. Each new proof checker accepts new kinds of proof steps which were not accepted in the previous levels. By taking advantage of these new proof steps, higher-level proofs can be written more concisely than lower-level proofs, and can take less time to construct and check. Our highest-level proof checker, Level 11, can be thought of as a simplified version of the ACL2 or NQTHM theorem provers. One contribution of this work is to show how such systems can be verified. To establish that the Level 11 proof checker can be trusted, we first use it, without trusting it, to prove the fidelity of every Level n to Level 1: whenever Level n accepts a proof of some phi, there exists a Level 1 proof of phi. We then mechanically translate the Level 11 proof for each Level n into a Level n - 1 proof---that is, we create a Level 1 proof of Level 2's fidelity, a Level 2 proof of Level 3's fidelity, and so on. This layering shows that each level can be trusted, and allows us to manage the sizes of these proofs. In this way, our system proves its own fidelity, and trusting Level 11 only requires us to trust Level 1.

Recent planning and scheduling applications have successfully used the Temporal Constraint Satisfaction Problem (TCSP) to model events and temporal constraints between them. Given a TCSP, the task is to find a schedule or a set of schedules that satisfy all constraints in the problem. A key limitation of TCSPs and related formulations is that they only represent hard constraints---constraints that are either satisfied or not. Many real-world situations are better modeled with soft constraints---constraints that are satisfied to a particular degree. Soft constraints allow knowledge engineers to express that some situations are preferable to others. This dissertation augments TCSPs with soft constraints and presents algorithms that find optimal solutions. We represent soft constraints by augmenting hard constraints with a preference function that maps every valid solution to a local preference value that describes how well the constraint is satisfied. We then aggregate the local preference values to attain the value of the entire solution. We studied two aggregation functions, the sum and minimum functions. We developed a set of algorithms that optimize with respect to both aggregation functions when preferences are added to each of two common TCSP subproblems: the Simple Temporal Problem (STP) and the Disjunctive Temporal Problem (DTP). We analyzed each algorithm experimentally on random problems and showed that the algorithms for DTPs with preferences integrate practically into a planning and scheduling application called Autominder. Before integration, we modified the algorithms to handle dynamic DTPs with preferences, equipping them to solve a series of related DTPs with preferences faster than solving them individually. In many real-world problems, finding the optimal solution is not necessary---it is more important to find near-optimal solutions quickly. Consequently, our focus was on maximizing anytime performance. We achieved this goal, showing empirically that our algorithms quickly found high-quality solutions even for large problems. For all algorithms, we showed that the cost of adding preferences was minimal, achieving our overall goal of making the use of TCSPs with preferences practical in all situations where hard-constraint TCSPs apply.