[Colloquium] Reminder: Guest Speaker @ TTI-C Today (5/2/06)

[Katherine Cumming]

**********TTI-C Guest Speakers This Week***********
                                    May 2, 2006
        Presented by:  Toyota Technological Institute at Chicago
 
 
(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 
 
 
 
----------------------------------------------------------------------------
------
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/20060502/678b5c52/attachment.htm