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

[Katherine Cumming]

**********TTI-C Guest Speaker Today***********
                             March 8, 2006
        Presented by:  Toyota Technological Institute at Chicago
 
 
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. 
 
----------------------------------------------------------------------------
------
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/20060308/8b5166f8/attachment.htm