Subject: Talk abstract
           Research Opportunities in Verification Engineering
Status: RO

{\em Model checking} is powerful technique for verifying hardware and software
systems, especially safety critical systems such as implantable medical
devices, nuclear power plant control software, etc.  Until recently, such
verification activity has been carried our in relative isolation, separate
from the traditional software lifecycle, which involves, among other things,
design, specification, coding, testing, and maintenance.
Our research on model checking and verification in general is concerned with
ameliorating this problem by integrating verification into the lifecycle model.
The goal is to make verification more of an {\em engineering} discipline, on
par and equal to software engineering.  The approach Professor Rance Cleaveland
and I are following is manifest in the Concurrency Factory, a graphical
environment for the design, simulation, verification, and implementation of
concurrent and distributed systems.

In this talk I will discuss several research opportunities for MS students
seeking CSE 523/524 projects or PhD students seeking PhD thesis topics.  These
include a joint project with the Oregon Graduate Institute on the verification
of specifications of microprocessors at the microarchitectural level, and the
specification and verification of the Internet Control Message Protocol
(ICMPv6) for the Internet Protocol Version 6 (IPv6).  Funding is available, in
the form of Research Assistantships, for qualified students.
For more information about the Concurrency Factory, please see:
  http://www.cs.sunysb.edu/~concurr
  http://www.cs.sunysb.edu/~ysr/wrkshp/wrkshp.html
  http://www.cs.sunysb.edu/~clubconc
  http://www.cs.sunysb.edu/~sas
For an overview of Concurrency Theory, the theory behind the Concurrency
Factory, please see:
  
  http://www.cs.sunysb.edu/~sas/sdcr/report/final/final.html