## SSS Abstracts |

This is a joint work with Geoff Gordon and Sebastian Thrun.

This talk is in partial fulfillment of the speaking requirement.

This talk is in partial fulfillment of the speaking requirement.

This talk presents a new approach to building scalable and automated decision procedures for first-order logics involving arithmetic. There are two key ideas in this approach. First, decision problems involving arithmetic are transformed to problems in the Boolean domain, such as Boolean satisfiability solving, thereby leveraging recent advances in Boolean methods. Second, the transformation automatically detects and exploits problem structure, using formula analysis and machine learning. Decision procedures based on these problem-specific Boolean methods can outperform other state-of-the-art procedures by two or three orders of magnitude.

This approach has been implemented in two systems, UCLID and TMV, and its utility has been demonstrated in a range of applications, including finding API-level security exploits, detecting viruses and worms, and verifying circuits that operate under timing assumptions.

This talk is in partial fulfillment of the speaking requirement.

This talk describes a new approach to the scalability of task management in space, across heterogeneous computing environments, and in time. The approach is based on high-level models of what users need from the computing environment for each of their tasks. Such models are exploited at run-time by an infrastructure that automatically configures the computing environment on behalf of users.

We present an architectural framework that grounds our approach, and a utility-theoretic model that enables finding the best match between user needs and the capabilities and resources in the environment.

In this paper we introduce multi-splay trees, which can be viewed as a variant of splay trees. We prove the multi-splay access lemma, which resembles the access lemma for splay trees. With different assignment of weights, this lemma allows us to prove various bounds on the performance of multi-splay trees. Specifically, we prove that multi-splay trees are O(log log n)-competitive, and amortized O(log n). This is the first BST data structure to simultaneously achieve these two bounds. In addition, the algorithm is simple enough that we include code for its key parts.

This talk is in partial fulfillment of the speaking requirement.

This talk is in partial fulfillment of the speaking requirement.

To avoid interaction failures, a dependable user interface must facilitate task completion as quickly and as accurately as possible. Defects in the interface cause user errors (e.g., goal, plan, action and perception errors), that impinge on accuracy goals, and can lead to mission failure.

This paper seeks the causes of goal errors, asking what aspects of a user interface contribute to or detract from a user's propensity to commit goal errors. A design procedure (external subgoal support) was formulated for helping prevent goal errors. Implementing this procedure requires identifying the information needed to set and verify completion of subgoals, and presenting the user with a salient representation of this information. Two interfaces for setting user file permissions were tested: Windows XP and an alternative. The alternative was designed using external subgoal support, and Windows was not. Experiments with 24 human subjects demonstrated the increased effectiveness of the alternative interface, obtaining as much as a four-fold increase in accuracy in a representative user task, and a 94% reduction in the number of goal errors committed.

This talk is in partial fulfillment of the speaking requirement.

We present a data-driven, instance-based approach to question answering (IBQA) in which we learn how to answer new questions from similar training questions with known correct answers. We cluster the training questions according to different granularity, scatter, and similarity metrics. From each cluster we automatically learn an "answering strategy" for finding answers to questions in that cluster. When answering new questions, multiple answering strategies are simultaneously employed.

The IBQA approach is resource non-intensive, but can easily be extended to incorporate knowledge resources or rule-based components. Since it does not rely on hand-written rules, expert knowledge, and manually tuned parameters, it is less dependent on specific languages and domains, allowing for fast re-training with minimum human effort. Even with limited data, IBQA achieves good performance, improves with additional training instances, and is easily trainable and adaptable to new types of data.

This talk is in partial fulfillment of the speaking requirement.

Datasort and index refinements allow programmers to specify stronger properties through the static type system: (1) Datasorts refine algebraic datatypes through a finite subsorting relation (for example, empty lists are included in even lists; even-length lists and odd-length lists are included in all lists). (2) Indices refine datatypes by elements of some decidable constraint domain, such as linear inequalities over integers (for example, trees indexed by an integer denoting the number of non-leaf nodes).

Typechecking in a system with datasort and index refinements proves at compile time that functions have the properties specified by the programmer: that the offset given to an array-access primitive is in range, that color and black height invariants of red-black trees are preserved, and so forth.

This talk focuses on how to identify properties expressible through refinements, and how to define and use appropriate refinements.

This work unifies and extends previous work on datasort refinements, index refinements, intersection types, and union types.

This is joint work with Frank Pfenning.

This talk is in partial fulfillment of the speaking requirement.

In this talk I will review the general setup of the optimal combinatorial auction design problem. I will also introduce one of the promising approaches to the problem, which focuses on designing approximations (suboptimal auction mechanisms which yield high revenue) rather than attempting to characterize the optimal mechanism itself. Finally I will present the approximation results obtained in worst-case and average-case frameworks.

This talk is in partial fulfillment of the speaking requirement.

We present a minimal functional language with explicit mobility and locality types which safely "strain out" these localized resources. Mobile code and values are given the type []A (meaning "anywhere A") and remote resources the type <>A (meaning "somewhere A"). The calculus allows both spawning mobile code for evaluation anywhere, and non-local control transfers for access to remote resources. This by no means exhausts the rich variety of mechanisms for distributed programming introduced in prior work. Rather, it serves as a natural, simple demonstration of the type-soundness of the approach, and a laboratory in which to consider various language extensions.

The calculus is "low-level" in the sense that location abstraction is sacrificed (somewhat) to obtain safety. The programmer must be aware of whether a resource is here or elsewhere, whether a fragment of code is mobile or not. But in exchange, he/she gets marshalling safety and more predictable performance. A little bit of effort for a tasty result!

Joint work with Frank Pfenning.

This talk is in partial fulfillment of the speaking requirement.