[Prev][Next][Index]

dar seminar - next two weeks and John Field visiting

Since many people will be at various conferences next week, yet we do
not want to cancel our seminar a second time:), we decided to move
next Wednesday's seminar to the following Monday.  So there will be no
seminar next week, and there will be two seminars the week after:

Mon Dec 3, 11am, Michael Kifer will be our speaker;
Wed Dec 5, 2pm, John Field (IBM Watson) will be our speaker.
		(http://www.research.ibm.com/people/j/jfield/)

Below is John's talk abstract.  If you would like to meet with him
during his visit, please let me know what times are good for you on
that day.  He is also interested in meeting Ph.D. students (especially
those near graduation) working in areas related to programming
languages, compilers, and related systems (including in particular,
program analysis, languages for distributed systems, verification).

Annie
--
	     Deriving Specialized Program Analyses for
	      Verifying Component-Client Conformance

			    John Field
		  IBM T.J. Watson Research Center

A fundamental impediment to effective use of software components or
libraries is ensuring that client codes satisfies the _constraints_
that the component imposes as a prerequisite to correct usage.  The
Canvas project at IBM Research and Tel-Aviv University
(http://www.research.ibm.com/menage/canvas/) aims to ease the use of
software components by allowing the component designer to specify
component _conformance_ constraints in a natural way, and providing
the client code developer with automated software certification tools
to determine whether the client satisfies the component's conformance
constraints.

In this talk, we show how static conformance certification can be
efficiently carried out in a _staged_ manner for certain classes of
conformance constraint specifications.  In the first stage, we derive
a component-specific set of abstractions for use in analysis of
arbitrary clients.  Unlike verification approaches that analyze a
specification and client code together, our technique can take
advantage of computationally-intensive symbolic techniques without
affecting the performance of client analysis.  In the second stage,
the generated abstractions are incorporated into a static analysis
engine to produce a _certifier_.  In the final stage, the resulting
certifier is applied to a client to conservatively determine whether
the client violates the component's constraints.

This work is joint with G. Ramalingam, Alex Warshavsky, Deepak Goyal,
and Mooly Sagiv.