Message-ID: <4E06A937DADC3842ACE4D3A1096A9EAC0384DC@JANUS.eecs.berkeley.edu>
From: George Necula <necula@EECS.Berkeley.EDU>
Subject: Next Monday: PS Seminar
Date: Mon, 22 Oct 2001 12:52:28 -0700
Hi,
Next Monday we will be visited by John Hatcliff, one of the creators of the
Bandera tool for model checking Java programs. He will give a talk at 4pm
(October 29) in Soda 310 in the Programming Systems Seminar. He is also
anxious to meet with faculty and students on Monday and (possibly) on
Tuesday. Please send your preferred times to Liliana
(lilianag@cs.berkeley.edu).
George.
==========================================================================
Talk Title: Model-checking Concurrent Java Software
Using the Bandera Tool Set
Speaker: John Hatcliff,
Kansas State University
Finite-state verification techniques, such as model checking, have been an
effective means for finding subtle defects in hardware designs. The
increased use of concurrent software in embedded applications and the
widespread adoption of Java with its built-in concurrency constructs have
led researchers to attempt to adapt model-checking techniques to software.
To date, this effort has been hindered by several obstacles including
construction of correct tractable models from programs with enormous state
spaces, appropriate specification of checkable software requirements, and
interpretation of very long counterexample traces.
In this talk, we describe Bandera -- an integrated collection of tools for
model-checking concurrent Java software that attempts to overcome the
obstacles described above. Bandera is a model compiler in the sense that it
takes Java source code as input and compiles it to a program model expressed
in the input language of one of several existing verification tools
including SMV, Spin, dSpin, and JPF. Program slicing and abstract
interpretation components are used during compilation to customize the
program model with respect to the properties being checked. Bandera is like
a debugger in the sense that it maps counterexamples produced by back-end
model checkers back to the source code level, and it allows the user to
replay program execution both forwards and backwards along the path of the
counterexample.
We illustrate the functionality Bandera's major components with some simple
examples and give an overview of how Bandera's extensible temporal property
specification language can be used to specify temporal properties in terms
of Java source code features. We conclude with a discussion of other forms
of automated tool support that we are currently working on that we believe
are necessary for model-checking properties of large code bases.
Bandera Project Web site: http://www.cis.ksu.edu/~santos/bandera
URL of a paper closely related to the talk:
http://www.cis.ksu.edu/~hatcliff/Papers/bandera.ps.gz
This archive was generated by hypermail 2b30 : 11/04/02 PST