CS Department Colloquium Series

Software is everywhere, and yet, extremely unreliable. One key to reliability is the design of cost-effective techniques whereby developers can formally specify essential properties of their code, and, machines can rigorously verify that the properties hold, or demonstrate corner cases where they fa

Today's computers run numerous processes of different sensitivity and trustworthiness, and often the only boundary between a hostile network and sensitive data relies on flimsy confinement assumptions.

Since the 1960s at the latest, the computer has been capable of digitally synthesizing any perceivable sound. However, in a live context, human-computer interfaces limit the bandwidth and quality of the interaction between the performer and the sound synthesizer.

Reconstruction of trees describing relationships among species is of vital importance to evolutionary studies. Species trees not only reveal the history of life, they also provide a framework for understanding the evolution of physiology, morphology, and cellular circuitry.

Given a query where the answer is sitting on a single web page, search engines do a decent job of identifying that web page. Some queries, however, are difficult to express in text: an image is worth a thousand query terms.

Molecular sequences evolve under processes that include substitutions, insertions, and deletions (jointly called "indels"), as well as other mechanisms (e.g., duplications and rearrangements).

PlanetLab was originally designed to be a realistic testbed for networking and distributed systems research. It has served that role quite well.

Assertions are widely used for runtime checking of software correctness, and increasingly used for compile time checking of simple properties like array index bounds.

Over time PlanetLab has evolved from a centrally-administered testbed to a federation of regional testbeds that are operated independently. The PlanetLab software is also freely available, which has allowed many organizations to bring up their own "private" PlanetLabs.

This talk introduces a new class of methods called "behavioral blacklisting", which identify spammers based on their network-level behavior.