[Colloquium] Guest Speakers @ TTI-C Next Week (3/6/06-3/10/06)

Fri Mar 3 16:11:40 CST 2006

**********TTI-C Guest Speakers (4) Next Week***********
                      March 6 - March 10, 2006
        Presented by:  Toyota Technological Institute at Chicago

(1)

Speaker: Emanuele Viola, Harvard University
Speaker's home page: http://www.eecs.harvard.edu/~viola/

Date: Monday, March 6, 2006 
Location: TTI-C Conference Room
Time:  10:00 am 

Title:  Derandomization: New Results and Applications
Abstract:
Randomness has proven to be a valuable resource throughout computer science.
In particular, there are several fundamental computational problems that we
know how to solve efficiently only when we have a source of randomness at
our disposal.  But to what extent is randomness really necessary for
efficient computation?

In this talk, we survey some of our results in derandomization, which is the
field that studies the possibility and implications of simulating randomized
computation deterministically.

First, we address the derandomization of restricted computational models,
focusing on constant-depth circuits.  We develop a new application of the
derandomization of constant-depth circuits to the study of the average-case
complexity of NP.  In particular, we show how to take any function in NP
that is `mildly' hard on average and transform it into one that is
`extremely' hard on average.  We also obtain a new sub-exponential time
derandomization of constant-depth circuits with few majority gates.  This is
currently the richest randomized circuit class that researchers can simulate
in sub-exponential time.

We then discuss the derandomization of general computational models.  For
general models, the only non-trivial derandomization known is the '83 result
that probabilistic polynomial time (BPP) can be simulated in the second
level of the polynomial-time hierarchy.  Perhaps surprisingly, in more than
two decades no work has addressed the running time of this simulation.  In a
recent work, we prove that a quadratic slow-down in running time is inherent
in this simulation (for relativizing techniques).  However, as our results
show, this quadratic slow-down disappears at the third level of the
polynomial-time hierarchy, and a quasilinear-time simulation becomes
possible.

No previous knowledge of complexity theory is required for this talk. 

(2)

Speaker:  Seth Pettie, Max Plank Institute
Speaker's home page: http://www.mpi-sb.mpg.de/~pettie/

Date: Tuesday, March 7, 2006 
Location: TTI-C Conference Room
Time:  10:00 am

Title: Finding the Shortest Path
Abstract:
What's the shortest route from point A to point B? This is a fundamental
algorithmic question with deep connections to other optimization problems
and numerous practical applications. The most well known applications are
services like Google Maps, OnStar, and MapQuest, which will quickly answer
shortest path queries on the U.S. road network. Although shortest path
algorithms are relatively fast in practice, the inherent time complexity of
computing shortest paths is unresolved. In fact, on general graphs this
problem has seen surprisingly little progress since the invention of the
"textbook" algorithms of Dijkstra, Bellman-Ford, and Floyd-Warshall in the
late 1950s.

In the first part of this talk, I'll present an asymptotically faster
all-pairs shortest path algorithm for general graphs. This is the first such
algorithm to improve the running time of Dijkstra's algorithm.

In many scenarios, finding shortest paths is only the beginning. The more
challenging problem is to encode shortest path information in a succinct and
usable way. (For instance, in the form of routing tables distributed across
the nodes of a network.) In the second part of the talk, I'll discuss my
work on low-distortion spanners, which are objects that efficiently encode
approximately shortest paths. 

(3)

Speaker:  Viktor Kuncak, MIT CSAIL
Speaker's home page: http://www.mit.edu/~vkuncak/

Date: Wednesday, March 8, 2006 
Location: TTI-C Conference Room
Time:  10:00am

Title:  

Modular Static Analysis with Sets and Relations
Abstract:
We present a new approach for statically analyzing data structure
consistency properties. Our approach is based on specifying interfaces of
data structures using abstract sets and relations.

This enables our system to independently verify that
1) each data structure satisfies internal consistency properties and each
data structure operation conforms to its interface;
2) the application uses each data structure interface correctly, and
maintains the desired global consistency properties that cut across multiple
data structures.

Our system verifies these properties by combining static analyses,
constraint solving algorithms, and theorem provers, promising an
unprecedented combination of precision and scalability. The combination of
different techniques is possible because all system components use a common
specification language based on sets and relations.

In the context of our system, we developed new algorithms for computing loop
invariants, new techniques for reasoning about sets and their sizes, and new
approaches for extending the applicability of existing reasoning techniques.

We successfully used our system to verify data structure consistency
properties of examples based on computer games, web servers, and numerical
simulations. We have verified implementations and uses of data structures
such as linked lists with back pointers and iterators, trees with parent
pointers, two-level skip lists, array-based data structures, as well as
combinations of these data structures. This talk presents our experience in
developing the system and using the system to build verified software. 

(4)

Speaker: Matthew Fluet, Cornell University
Speaker's home page: http://www.cs.cornell.edu/people/fluet/

Date: Thursday, March 9, 2006 
Location: TTI-C Conference Room
Time:  10:00am
Title:  Type-systems for Resource Conscious Programs
Abstract:
Resources, such as file descriptors or memory, are precious commodities in
computations. Improper use of a resource, such as reading from a closed file
or accessing deallocated memory, can be the source of many program bugs.
Yet, conventional languages and type systems cannot statically identify
these improper uses as potential points of failure. In contrast, type
systems for resource conscious programs are designed to statically catch
improper uses of resource primitives. My research has focused on improving
the type systems for resource conscious programs.

In this talk, I'll review some problematic uses of resources before
examining three "flavors" of type systems: * an established type-and-effect
system (a la Gifford-Jouvelot and Tofte-Talpin) * a novel monadic type
system * a novel substructural type system. The monadic type system draws
inspiration from (and generalizes) the state monad of Launchbury and Peyton
Jones. This monadic type system trades the subtleties of the type-and-effect
system for the simplicity of a monadic system, where plain old parametric
polymorphism (a la System F) provides sufficient encapsulation.

However, both the type-and-effect system and the monadic type system require
that resources have last-in-first-out (LIFO) lifetimes following the block
structure of the program. The substructural type system eliminates this LIFO
restriction. The key idea is to separate the lifetime of a resources from
the scope of the resource's name, by providing explicit resources creation
and destruction primitives. Finally, I'll examine some promising
applications of these systems.
----------------------------------------------------------------------------
------
If you have questions, or would like to meet the speaker, please contact
Katherine at 773-834-1994 or kcumming at tti-c.org.   
For information on future TTI-C talks and events, please go to the TTI-C
Events page:  http://www.tti-c.org/events.html.  TTI-C (1427 East 60th
Street, Chicago, IL  60637)

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20060303/f67b351a/attachment.htm