[Colloquium] Guest Speaker

[Ponda Barnes]

 TTI-C Guest Speaker
 
Presented by: Toyota Technological Institute at Chicago
 
Speaker: Jia Limin
Speaker's home page: http://www.cs.princeton.edu/~ljia/
 
Date:  Tuesday, March 13, 2007
Location: TTI-C Conference room
Time: 10:00am
 
Title: Linear Logic and Imperative Programming
 
Abstract:
 
Improper pointer operations in software written in programming languages
such as C significantly compromise the reliability and security of software
systems.  Therefore, one of the most important and enduring problems in
programming languages research involves verification of programs that
construct, manipulate, and dispose of complex heap-allocated data
structures.  In my talk, I will first present our new sub structural logic
for reasoning about the memory safety of imperative programs. Our new logic
modularly integrates sub structural reasoning with constraint-based
reasoning such as integer constraints. 
Next, I will introduce a new imperative language that allows programmers to
define and manipulate recursive data structures using formulas in our logic.
By combining new verification techniques based on sub structural logics with
a modern type system for resource control, this language guarantees not only
the memory safety of operations such as deallocation and dereferencing, but
also ensures that shape invariants of data structures hold throughout the
execution of the program.
 
If you have any questions or would like to meet the speaker, please contact
Ponda Barnes at pondabarnes at tti-c.org
For future TTI-C talks and events, please go to
http://ttic.uchicago.edu/cal/month.php
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20070312/26bc8523/attachment.htm