[Prev][Next][Index]

dar seminar - John Field: Deriving Specialized Program Analyses ...

John Field will be our speaker tomorrow afternoon.  He is manager of
the program analysis group (now more on checking and certifying
software) at IBM Watson (one of the basically two research labs left
in industry :-().  Everyone is welcome.  John gives nice and clear
talks :-).

John is interested in meeting people, including 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, and
verification).  He has a quite full schedule already, but if you would
still like to meet him, let me know your time constraints and I will
try to fit you in.

		 Design and Analysis Research Seminar
                         Wed., Dec. 5, 2001
                     2-3pm, CS Seminar Room 1306

	      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.