Mathematics & Computer Science

Seminars and Colloquia

Computer Science Seminar

Tuesday, November 18, 2014

04:15 pm - 05:30 pm

CS Seminar, Dan Fasulo (Pattern Genomics): DNA signatures - An idea whose time has finally come

Abstract:<br/><br/>DNA signatures are short nucleotide sequences that uniquely identify a class of target organisms such as a specific bacterial species or viral strain. Algorithms to find DNA signatures have been described in bioinformatics literature for over a decade, but only recently has the widespread adoption of next generation DNA sequencing made it feasible for a typical molecular biology laboratory to mine large collections of DNA sequences for signatures. This talk will discuss algorithms for finding DNA signatures and describe how these techniques are poised to revolutionize molecular diagnostics.<br/>

ESC 638

Tuesday, November 11, 2014

04:15 pm - 05:30 pm

CS Seminar, John Karro (Univ. of Miami Ohio): The identification and analysis of genomic transposable elements.

Abstract: Transposable Elements, or TEs, are mobile DNA sequences capable of inserting multiple copies of themselves into a genome. Throughout our evolutionary history the human genome has been repeatedly subjected to such insertions, to the point where upward of 45% of our genetic sequence is the remnants of TEs and other repetitive sequences. Identifying these TEs could be easily framed as a basic string-matching problem, were it not for the effect of genetic mutations: while a given TE was initially a copy of its progenitor sequence, over time the DNA sequence changed in an apparently random manner. Thus the identification problem becomes significantly more difficult, and is even further complicated by size of the input which any solution algorithm will be applied. Given the size of the higher-order genomes (e.g. n ≈ 3?109 for human, n ≈ 5x1010 for salamander), any identification algorithm must have runtime and memory usage bounds that scale linearly with input size if the algorithm is to be of practical use. But once TEs have been identified, they provide important information on the very mutation rates that made them so hard to identify ? giving us a window into genomic evolutionary history.<br/><br/>This talk will explore how and why we are solving the identification problem. We will describe the algorithm underlying RAIDER, a new tool for the fast de novo identification of transposable elements. Following this we will describe a mathematical model of molecular evolution, based on TE information that will allow for the identification of genes that have undergone a change in their strand-symmetry classification sometime over the last one-hundred million years.<br/><br/>Note: This talk will assume an audience with a background in mathematics or the quantitative sciences. No knowledge of biology will be required, though some may be inflicted.

ESC 638

Wednesday, March 26, 2014

01:30 pm - 02:30 pm

Computer Science Seminar, Danny Krizanc (Wes): "Mobile Agent Rendezvous"

Abstract:<br/><br/>Alpern (1976) is credited with asking the following question:<br/>Two astronauts land on a large spherical body. The body has no fixed orientation in space, no axis of rotation, so that no common notion of position or direction is available to the astronauts. Given unit walking speeds how should they move about so as to minimize the expected time until they meet?<br/><br/>This has lead to a great deal of research on so-called "rendezvous" problems. This talk will survey a small portion of this research as it has developed in the study of mobile agents.<br/>

ESC 618

Wednesday, February 26, 2014

01:30 pm - 02:30 pm

Computer Science Seminar, Henny Admoni (BA'08 MA'09, Yale University): "The Role of Eye Gaze in Social Robotics"

Abstract: Eye gaze is an important component of human social interaction, and is therefore a key element in the design of robots that interact in social environments with people. Experiments investigating eye gaze in human-robot interactions have shown that robot gaze is often interpreted in similar ways to human gaze, facilitating efficient non-verbal communication between robots and humans. However, on a cognitive level, robot gaze fails to cue reflexive human attention, indicating that some difference exists between how people process eye gaze from humans and from robots. My research focuses on modeling human gaze behavior and understanding how these models differ when applied to robots. This research has applications in a variety of areas that involve robots interacting with people, particularly for socially assistive robots.<br/><br/>Bio:<br/>Henny Admoni (BA '08 MA '09) is a PhD candidate and a member of the Social Robotics Laboratory in the Department of Computer Science at Yale University, where she is advised by Professor Brian Scassellati. Henny creates and studies robots that interact closely with people, and her research is about how to leverage non-verbal social cues, such as eye gaze, to make these human-robot interactions more effective. More information can be found at http://hennyadmoni.com.<br/>

ESC 618

Tuesday, February 11, 2014

04:15 pm - 05:30 pm

CS Seminar, Ran Libeskind-Hadas (Harvey Mudd College): "The Hitchhikers Guide to Coevolution"

Abstract: In the "Origin of Species," Darwin speculated that the evolution of one species could effect the evolution of another. For example, bees and flowers might have coevolved in a mutually beneficial way. In other cases, a parasitic species might track the evolutionary history, or "hitchhike", on its host species. In recent years, computational methods have been developed that allow biologists to study if and how pairs of species might have coevolved. In this talk, I will describe the computational problems, algorithmic solutions, and the resulting software systems that have been developed to study coevolution, offering several examples of how these computational tools have led to interesting discoveries.<br/><br/>Bio: Ran "RON" Libeskind-Hadas is the R. Michael Shanahan Professor of Computer Science at Harvey Mudd College. He received the A.B. in applied mathematics at Harvard University and the M.S. and Ph.D. in computer science at the University of Illinois at Urbana-Champaign. His research interests are in algorithms and computational biology. <br/>

ESC 638

Tuesday, November 19, 2013

12:00 pm - 01:00 pm

Computer Science Seminar: Howard Blair, Syracuse University

Abstract: The relatively recent developments that exploit quantum phenomena for computing faster and communicating more securely have re-energized research into the basics of quantum phenomena and are forcing researchers to confront the problem of explaining how the world can actually be the way we observe it to be: The world is quantum mechanical.<br/><br/>The talk will present an overview of:<br/> * Qubits(quantum bits)<br/> * Quantum registers<br/> * Quantum state transitions<br/>and will review several well-known results that argue for the nonexistence of definite quantum states until a measurement is made.<br/>The talk will also sketch Abramskya'™s simple imperative quantum programming language as a practical tool for prototyping code for quantum algorithms, with consequences for proving quantum programs correct and for algorithm complexity.<br/><br/>"€œAnyone who is not shocked by quantum theory has not understood it."<br/> -€“Niels Bohr<br/><br/>Prof. Blair teaches undergraduate and graduate courses in quantum computing in the Department of Electrical Engineering and Computer Science at Syracuse University. He conducts research in software and hardware verification and validation of classical and quantum computing systems as well as hybrid discrete/continuous dynamical systems. In these endeavors he collaborates with computer scientists, mathematicians, biologists, physicists and philosophers at Syracuse University and other universities and at the U.S Air Force Research Laboratory in Rome, NY.<br/>

ESC 638

Tuesday, November 12, 2013

04:15 pm - 05:30 pm

Computer Science Seminar: Richard Silverman (D.E. Shaw)

Title: Basics of IP routing: Distance-vector vs. link-state approaches<br/><br/>When you launch a packet of data onto the Internet, how does it get where it's going? At each hop along the path to its destination, a network device called a router forwards the packet along, but how does each router know the best way to send a given packet to any of several billion possible addresses? Does each router have a complete map of the Internet? If not, how can it make these decisions? And, what happens if the network changes: if a path stops working, or a new one becomes available?<br/><br/>To deal with these issues, we have dynamic routing protocols: mechanisms which allow routers to discover each other, find and maintain optimal paths to all reachable destinations, deal with link failures and additions, and more. In this talk, we will focus on the class of interior gateway protocols, and discuss the two dominant approaches to routing: distance-vector and link-state algorithms, as embodied in the RIP and OSPF routing protocols.<br/><br/>Since earning his B.A. in computer science and M.A. in pure mathematics, both at Wesleyan University, Richard Silverman has worked in the fields of networking, formal methods in software development, computer security, and Unix systems administration. He has co-authored two books on computer security published by O'Reilly: SSH, The Secure Shell (The Definitive Guide), and the Linux Security Cookbook. He is currently on the engineering staff of D. E. Shaw & Co., L.P., a company focused on areas it believes can be fundamentally altered by the application of computing technology -- in fields ranging from finance to molecular biology.

ESC 638

Tuesday, October 29, 2013

04:15 pm - 05:30 pm

Computer Science Seminar: Arjun Guha (UMass Amherst)

Title: Reclaiming security for web programmers<br/><br/>Abstract: The Web enables new classes of programs that pose new security<br/>risks. For example, because Web programs freely mix data and code from<br/>untrusted sources, major websites have been compromised by third-party<br/>components, such as malicious ads. In addition, users cannot fully<br/>control which programs run; Web programs are visited, not installed.<br/>Therefore, Web security is entirely in the hands of programmers, not<br/>users.<br/><br/>I address the problem of securing existing Web programs, which are<br/>universally written in JavaScript. Unfortunately, JavaScript has<br/>several warts that make it difficult to reason about even simple<br/>snippets of code. Several companies have developed "Web sandboxes" to<br/>make JavaScript programming safe. However, these Web sandboxes have no<br/>security guarantees.<br/><br/>In this talk, I show how programing languages research can be used to<br/>verify properties of Web applications. I present a type-based<br/>verification method for JavaScript that we use to find bugs in and<br/>produce the first verification of an existing, third-party Web sandbox.<br/><br/>Programming language techniques can give us mathematical proofs of<br/>security, but attackers attack implementations, not theorems. I discuss<br/>our approach to doing principled, real-world Web security research,<br/>which combines semantics with systems. I also review additional projects<br/>that use our tools and techniques.<br/><br/><br/>Bio: Arjun Guha is an assistant professor of Computer Science at UMass<br/>Amherst. He enjoys tackling practical problems, while adhering to the<br/>mathematical foundations of programming languages. For example, his<br/>dissertation on JavaScript semantics and type-checking, from Brown<br/>University, is used by several other researchers as a foundation for<br/>their own work. As a postdoc at Cornell University, he developed a model<br/>of software-defined networking (SDN) in the Coq Proof Assistant, which<br/>is the foundation for a verified runtime and other SDN tools. His<br/>research has led to several software systems, such as LambdaJS,<br/>Frenetic, and Flapjax that are in active use.<br/>

ESC 638

Friday, October 11, 2013

01:15 pm - 02:15 pm

Computer Science Seminar: Jim Royer (Syracuse University)

Abstract: We investigate the notion of feasible computability over<br/>inductive structures (henceforth, data) and coinductive structures<br/>(henceforth, codata). Data includes: natural numbers, strings of<br/>characters, (finite) lists, (finite) trees, etc. Codata includes:<br/>various sorts of potentially infinite lists (streams) and potentially<br/>infinite trees. We also investigate simple typed programming formalisms<br/>that attempt to capture feasible computability over data and codata.<br/><br/>Pinning down ``feasible computability'' over data and codata and<br/>capturing it in a programming formalisms turn out to be a subtle problem<br/>for which there is not yet a final answer. The present work focuses on<br/>bettering our understanding these problems and crafting tools to deal<br/>with them.<br/><br/>We start by introducing some simple classical systems for computing over<br/>data (via structural recursions) and codata (via structural<br/>corecursions) whose computational power goes well beyond the feasible.<br/>We rein in these systems by imposing a simple, two level ramification of<br/>their types (based on Bellantoni and Cook's normal/safe distinction).<br/>The resulting systems are nice and simple and a little surprising in<br/>what they compute and what they seem to fail to compute, especially in<br/>the codata realm.<br/><br/>The talk will be a tour through these various systems, focusing on<br/>motivations, definitions, examples, counterexamples, and open problems<br/>that our work reveals.<br/><br/>This is joint work with Norman Danner (Wesleyan University).

ESC 638

Tuesday, October 01, 2013

04:15 pm - 05:30 pm

Computer Science Seminar, Norman Danner (Wesleyan): Simulating (parts of) the Tor Network

Tor is probably the most widely-used anonymity network today. Because many people use it, new protocols cannot be tested on the deployed network, which makes it difficult to understand impacts and effects of proposed changes. This also affects our ability to understand possible attack vectors and defenses. Modeling and simulation of the network is therefore crucial. However, much research relies on simple models of both users and the network itself. I will discuss recent (and not so recent) investigations into more sophisticated simulation techniques, focusing on simulation of user behavior with hidden Markov models. I will in part be channeling Julian Applebaum '13, whose thesis contains much of this work.

ESC 638

Tuesday, September 17, 2013

04:15 pm - 05:15 pm

Computer Science Seminar, Megan Chang '14, Bree Lycette '15, Elliott Meyerson '14, Aaron Plave '15, Rachel Warren '14: What I did this summer.

Please join us as several of our students tell us about their various internships during Summer 2013: Megan Chang '14 at Blizzard; Bree Lycette '15 with the Hughes Program; Elliott Meyerson '14 at the USC ISI Natural Language Group; Aaron Plave '15 at the National Institutes for Health; and Rachel Warren '14 at Pandora Internet Radio.

ESC 121

Tuesday, April 09, 2013

04:30 pm - 05:30 pm

Computer Science Seminar, Kegan Samuel: "How do computers 'see'?"

Abstract: The human visual system can perceive and understand the world around with apparently very little difficulty. In the computer vision field, researchers attempt process and understand digital representation of images in a similar manner using various computer algorithms or mathematical models. While much has been accomplished in the field, there is still a significant amount of work to be done before a system is developed which would be able to interpret images at a level close to that of humans. <br/><br/>In addition to a brief overview of the problems encountered in the field of computer vision, I will also speak on work dealing with the use of Markov Random Field(MRF) models applied to the tasks of denoising and image segmentation. <br/>

ESC 638

Tuesday, May 01, 2012

04:15 pm - 05:30 pm

Computer Science Seminar, Stefan Sundseth '13: The Pi-Calculus for Mobile Systems

Abstract: In today's world computation revolves around interaction between multiple systems, yet the most well-known models of these computational systems neglect their ability to communicate with external processes. <br/>The Pi-Calculus was created as a means to rigorously describe a model whose fundamental action is to send and receive messages across an interface, which means that multiple processes can be synchronized by concurrent send/receive directives. Though simple, the Pi-Calculus is actually quite powerful as concepts such as algorithms, object-oriented programming, and the lambda-calculus fall within its scope.<br/>

ESC 339

Tuesday, April 24, 2012

04:15 pm - 05:30 pm

Computer Science Senior Thesis Talks: Jennifer Payking, Jeffrey Ruberg and Micah Wylde

Abstracts:<br/><br/>Jennifer Paykin: Automated Cost Analysis of a Higher-Order Language in Coq<br/><br/>The cost analysis of a program is a function from the size of its input to the number of steps the program takes to run. In this work we address two difficulties associated with constructing cost analyses. First, what is the cost of a higher-order program? If an expression takes a function as input, what is the size of that input? If an expression evaluates to a function, what is its cost? Second, how can we automate the cost analysis of arbitrary programs?<br/>In this work we develop a static cost analysis system for a functional target language with structural list recursion. A translation function maps target expressions e to complexities encoding upper bounds on both the cost of evaluating e and some measure of e's size. We implement the translation in the proof assistant Coq, formally verifying the soundness of the translation scheme. The resulting system generates certified upper bounds on the complexity of target language terms.<br/><br/><br/>Jeffrey Ruberg: Charming a Python with Static Type Checking<br/><br/>Pyty is a static typechecker for the Python programming language. Pyty imposes a static type system on users, for which they provide type declarations via comments. The type system developed is modeled on the Hindley-Milner type inference algorithm for the lambda calculus and its application to ML. Much of the implementation challenge is in applying this type system to a language not designed with typechecking in mind. <br/>The type system describes a system of deriving type assignments, whereby we can prove that a Python term can be assigned a specific type; we do this by searching for a valid tree of type assignment rules. Pyty also employs type inference for a restricted subset of the Python language in order to facilitate the typechecking algorithm.<br/><br/>Micah Wylde: Safe Motion Planning for Autonomous Driving<br/><br/>Self-driving cars have the potential to revolutionize transportation by making it cheaper, safer and more efficient. In this work we describe a novel motion planning system for translating high-level navigation goals into low-level actions for controlling a car. Specifically, the motion planning system is responsible for choosing at each time step an appropriate velocity and steering angle, which could then be implemented by the driving hardware or simulation. Our planner is able to compute a safe and efficient trajectory in a dynamic environment while staying within its lane and avoiding obstacles.<br/>

ESC 339

Tuesday, February 28, 2012

04:15 pm - 05:15 pm

Computer Science Seminar, Matt Eaton '04, Computer Science and Artificial Intetelligence Lab, MIT: "Chromatin and epigenetic regulation in DNA replication and Alzheimer's disease"

Abstract: In the nucleus of every eukaryotic organism, DNA is compacted and organized by wrapping around histone proteins in a structure called chromatin. Chromatin is a dynamic structure, and encoded in the histone tails are chemical modifications that provide clues to the underlying regulation of DNA-templated processes such as RNA transcription and DNA replication. This "histone code" can be measured genome-wide with high-throughput assays such as ChIP-sequencing.<br/><br/>A further layer of information is encoded in chemical modifications to the DNA itself; for example, cytosine residues in the genomes of higher eukaryotes can be methylated by nuclear proteins in heritable fashion, and this methylation can alter gene expression.<br/>Taken together, these layers of information encoded on top of the DNA sequence make up a large part of the field of epigenetics: the study of heritable, non-sequence, cis-acting changes to nuclear DNA and chromatin.<br/><br/>In this talk, I will give three examples of how machine learning and computer science techniques were used to help elucidate the epigenetic landscape in both model organisms and human disease. The first will examine the role of nucleosome positioning around origins of DNA replication in the genome of the budding yeast, Saccharomyces cerevisiae. The second example examines the role of the histone code in specifying the replication program of the fruit fly Drosophila melanogaster. Finally, I will discuss ongoing work in examining the role of DNA methylation in the cognitive decline of Alzheimer's disease patients.<br/>

ESC 113

Thursday, February 23, 2012

12:00 pm - 01:00 pm

(Computer Science Seminar) Matt Ginsberg, CEO On Time Systems, Inc: "Dr. Fill: Crosswords and An Implemented Solver for Singly Weighted CSPs"

Abstract: We describe and demonstrate Dr.Fill, a program that solves American-style crossword puzzles. From a technical perspective, Dr.Fill works by converting crosswords to weighted constraint satisfaction problems (CSPs), and then using a variety of novel techniques to find a solution. These techniques include generally applicable heuristics for variable and value selection, a variant of limited discrepancy search, and postprocessing and partitioning ideas. Branch and bound is not used, as it was incompatible with postprocessing and was determined experimentally to be of little practical value. Dr.Filll's performance on crosswords from the American Crossword Puzzle Tournament suggests that it ranks among the top fifty or so crossword solvers in the world.

ESC 339

Wednesday, November 30, 2011

04:15 pm - 06:00 pm

Dan Dougherty, Wes and Worcester Polytechnic Institute: Symbolic protocol analysis for implicitly authenticated Diffie-Hellman

Abstract:<br/><br/>Joint work with Joshua Guttman, WPI.<br/><br/>We develop new techniques for rigorous symbolic proofs of security<br/>properties for implicitly authenticated Diffie-Hellman protocols. These<br/>protocols, e.g.~{MQV} and the Unified Model, which construct a shared<br/>secret using a minimum of communication, have been challenging both for<br/>symbolic and computational analyses. Their essential use of rich<br/>algebraic structure has been an obstacle.<br/><br/>We prove implicit authentication and secrecy results for several<br/>protocols in this group. The same methods yield proofs of forward<br/>secrecy, for protocols where it holds, and indicate why it does not<br/>otherwise. Resistance to compromised key attacks and impersonation<br/>attacks may be resolved similarly.<br/><br/>Our crucial notion is the \emph{indicator}, a vector of integers that<br/>summarizes how many times each secret exponent appears in a message. We<br/>prove that the adversary can never construct a message with a new<br/>indicator in our adversary model.<br/><br/>Although we work with a message algebra generated by the normal forms<br/>for an equational theory $AG^$, we also give a model-theoretic proof<br/>that $AG^$ faithfully reflects all equations that are true uniformly as<br/>the prime $q$ varies. Hence, our security theorems ensure that the<br/>adversary has no strategy that is expressible algebraically and works<br/>uniformly---independent of the choice of $q$---for producing a<br/>counterexample. Computational soundness awaits further investigation.<br/>

ESC 638