[Colloquium] Guest Speakers @ TTI-C This Week (5/1/06-5/5/06)

[Katherine Cumming]

**********TTI-C Guest Speakers This Week***********
                             May 1 - May 5, 2006
        Presented by:  Toyota Technological Institute at Chicago
 
(1)
 
Speaker:  Yitzhak Mandelbaum, Princeton University 
Speaker's home page: http://www.cs.princeton.edu/~yitzhakm/
 
Date: Monday, May 1, 2006 
Location: TTI-C Conference Room
Time:  10:00 am   
Title:   The Theory and Practice of Data Description
Abstract:
Massive amounts of useful data are stored and processed in non-standard or
ad hoc formats, for which critical tools like parsers and formatters do not
exist.  Traditional databases and XML systems provide rich infrastructure
for processing well-behaved data, but are of little help when dealing with
data in ad hoc formats.  I will discuss my attempts to address the
challenges of ad hoc data with my work on the PADS project.  I will present
an introduction to PADS/ML, a declarative data description language that
permits analysts to describe the physical layout of their data and its
semantic properties.  From a description, the PADS compiler can
automatically generate a collection of useful data-processing tools for the
data source described, including parsing routines, statistical profiling
tools, and translators to standard formats like XML.  I will discuss the
formal semantics of the PADS language and two of its essential properties.
Finally, I will describe support for querying ad hoc data with the PADS tool
PADX.  I will discuss PADX from the user's perspective and review the main
challenges encountered in implementing PADX and their solutions.
 
(2)  
 
Speaker: Zhaozhong Ni, Yale University
Speaker's home page:  http://pantheon.yale.edu/~zn3/
 
Date: Tuesday, May 2, 2006 
Location: TTI-C Conference Room
Time:  10:00 am   
 
 Title:  Modular Machine Code Verification
 
Abstract:
 
Safety and efficiency are two highly desirable goals for software systems.
Unfortunately, under the current programming practice, they are difficult to
achieve at the same time.  This is especially true for system software.
Despite the progress made on safe languages and tools, a large and critical
portion of software, such as OS kernels, is still written in unsafe
languages.  One major reason is the lack of verification theories and tools
that can handle the expressive power of low-level code in a modular fashion.
In particular, many higher-order programming features, such as embedded code
pointer, are very difficult to handle in expressive low-level verification.
 
In this talk, I will present XCAP, a logic-based proof-carrying code
framework for modular machine code verification.  I will explain in detail
why embedded code pointer is a non-trivial problem and show how XCAP extends
the original CAP (certified assembly programming) to solve the problem.  I
will also show how XCAP supports other non-trivial features such as
impredicative polymorphisms, general references, and recursive
specifications.  I will then use a mini thread library written in x86
assembly to demonstrate how to certify OS-kernel level code in XCAP.  I will
also present a type-preserving translation from a typed assembly language to
XCAP, which demonstrates how to connect XCAP to existing higher-level
verification systems.
 
Bio: Zhaozhong Ni is a Ph.D. candidate in the Computer Science Department at
Yale University, where he is advised by Professor Zhong Shao.  He received
his bachelor's degree in computer science and technology from Tsinghua
University, Beijing in 2000.  His research interests include programming
languages and systems,
language-based security, type and logic systems for low-level program
verification, certified operating systems, and verification of concurrency
and multithreading 
 
 
(3)
 
Speaker:  Chris Wiggins, Columbia University
Speaker's home page:  http://www.columbia.edu/~chw2/ 
 
Date: Thursday, May 4, 2006 
Location: TTI-C Conference Room, Part of Bioinformatics Seminar
Time:  10:00am
 
Title:   Predictive Modeling of Network Evolution and Genetic Expression
 
Abstract:
 
High-throughput biological experiments now yield copious gene expression
data, sequence data, and network data, posing novel challenges to the
theoretical and computational community hoping to learn biology from these
abundant but heterogeneous datasets.  In this talk I hope to illustrate how
machine learning approaches can be brought to bear on two such network-level
problems in systems biology: `reverse-engineering` biological networks from
microarray and sequence data (including revealing sequence `motifs'), and
revealing which of several competing evolutionary design principles best
describes observed network topologies.  By posing these problems as
classification tasks, predictive and interpretable models are obtained.
Depending on whether the audience turns out to be computer scientists or
biologists, I will focus either on how to turn biology into boosting, or
vice versa. 
 
----------------------------------------------------------------------------
------
If you have questions, or would like to meet the speaker, please contact
Katherine at 773-834-1994 or  <mailto:kcumming at tti-c.org> 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/20060501/7798bdfe/attachment.htm