[Colloquium] Today's talk at TTI-C (Madhusudan Parthasarathy)

[Margery Ishmael]

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 Carole
  at cfkipp at tti-c.org