[Colloquium] Parthasarathy talk - Thurs. at 12:15 at TTI

[Meridel Trimble]

Toyota Technological Institute talk

Speaker: Madhusudan Parthasarathy 
Univ. of Pennsylvania

Date: Thursday, March 11th, 2004
Time: 12:15 pm
Place: TTI-C  (1427 E. 60th St.)
Refreshments provided

Title: Algorithmic Software Verification

Abstract: 
The rising need for reliable systems has spurred intense research in tools 
and techniques that aid detection of errors in programs.  A prominent paradigm 
is model checking: the automated formal verification of systems by state-space 
exploration.  Model-checking, aided with advances in automated abstraction, 
symbolic state-space exploration and boolean satisfiability solvers, is a 
paradigm that has proven to be effective in the hardware circuits domain. 

Modular programs, when abstracted, result in boolean pushdown models that can 
be model checked against classical specification logics such as linear temporal 
logic (LTL). However, LTL cannot express many interesting properties that are 
particularly relevant for software, such as correctness of procedures with 
respect to Hoare-style pre and post conditions, security properties that 
examine the call stack, etc.  We introduce CARET, a temporal logic of calls and 
returns, that can express such context-free properties and show that CARET can 
be model-checked with the same effort needed for LTL. 

The crucial aspect of CARET is that it ensures that specifications express 
pushdown properties only to the extent of matching calls and returns in the 
model.  Using this insight, we show a surprisingly robust subclass of 
context-free languages that subsumes regular languages and yet has all the 
desirable properties of regular languages that facilitate model-checking. 

In the final part of the talk, we present a new methodology for synthesizing 
interfaces for software modules.  The programmer of a module (or a class) 
intends a particular usage of the class that is often not formalized.  An 
interface to a class captures a formal set of rules of correct usage of the 
class.  We present the tool JIST (Java Interface Synthesis Tool) that extracts 
such interfaces using predicate abstraction, two-player games and symbolic 
exploration, and illustrate the paradigm with interfaces synthesized for some 
core Java2SDK library classes.

If you have questions, or would like to meet the speaker, please e-mail Meridel 
at mtrimble at tti-c.org