Message-ID: <4E06A937DADC3842ACE4D3A1096A9EAC0384E1@JANUS.eecs.berkeley.edu> From: George Necula <necula@EECS.Berkeley.EDU> Subject: CORRECTION: November 5: PS Seminar Date: Mon, 22 Oct 2001 13:05:02 -0700 Sorry, John Hatcliff seminar is on Monday November 5. George. > -----Original Message----- > From: George Necula > Sent: Monday, October 22, 2001 12:52 PM > To: 'languages@cs.berkeley.edu'; Open Source Quality Project > (softquality@eecs.berkeley.edu) > Subject: Next Monday: PS Seminar > > > > 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