[Colloquium] FW: Guest Speaker
Ponda Barnes
pondabarnes at tti-c.org
Tue Mar 13 09:03:01 CDT 2007
Reminder!!
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/20070313/d753a77b/attachment.htm
More information about the Colloquium
mailing list