To those students who would like to work on a research project with Dr. Subash Shanker (who teaches at Hunter College and the CUNY grad center) and me (D. Nixon), either in the summer and fall of 2001 or some future semester:

You may work on the project either for academic credit or just for the exaperience. You will not receive any money, but it will look very good on your resume -- especially if you are considering going for a Ph.D.

Our research is in the area of formal methods, an aspect of both software engineering and hardware engineering. Dr. Shankar has described the research as follows:

Formal verification is about the mathematical/logical modeling of computer systems so that they may be reasoned about. Systems can be software or hardware, and may be represented using any number of notations including programming languages, software specification languages (e.g., UML, Statecharts, RSML), [software] architectural description languages, and hardware description languages. Some applications of formal methods include automatic software restructuring (to make it better), software analysis, proof of correctness, and software reengineering.

Model checking is one of the most popular techniques for proving correctness. In model checking, one constructs a state machine equivalent to the system being verified, and then applies a model checking tool to prove properties about this state machine. Typical properties are liveness (state s is eventually reached) and safety (state s is never reached). There are several model checkers, but the big problem is state space explosion. If we use a naive approach, even a program with just 20 16-bit integer variables has 2^320 (approximately 10^100) states, which is about the limit of what can be verified.

One way to reduce this problem is by analyzing the source code and reducing the original program to a smaller program. Program slicing is one such technique. There are a few slicing tools available, though each of them does slightly different things, smoe of which may not be applicable.

In this project, we will start out by applying slicing for source code reduction, and studying how this helps formal verification. The longer term goals are to make model checking of software artifacts more feasible for real systems, without having to go through a manual process to simplify the system.

During the summer and fall of 2001, the main thing we will be doing is experimenting with a variety of already-existing software tools for model checking and program slicing, with the aim of identifying the shortcomings of these tools and recommending improvements. Eventually, Dr. Shankar would like me to develop a new tool, but it is unlikely that we will reach that point before the end of 2001. At the very beginning, we will also be reading and dicussing survey papars.

We will meet with Dr. Shankar at the CUNY Graduate Center (at 5th Avenue and 34th Street in Manhattan) approximately once every two weeks. Also, on the weeks in between meetings with Dr. Shankar, students working on the project will meet with me at Queens College.

The first program-slicing tool we will be using is Bandera, for which the documentation is here.

If you are interested, please E-mail me NOW, even if you are not yet qualified (as spelled out below). There will be some informal discussions held this summer, which you should attend even if you won't otherwise be qualified to help us for another year. Then, please contact me again sometime early in the semester just before the semester in which you will be qualified to help us.

To qualify, you will need to have taken at least CS 320 (or CS 721) and preferably also at least one subsequent computer theory course, such as CS 722 (if you are a master's degree student) or CS 323 (if you are an undergraduate student). (Note to M.A. students: See CS 721 or CS 722: Which To Take? on the Computer Science Department website.)

If you are an undergraduate with plans to go on to grad school, please consider taking CS 722 (for which you will need department permission) as well as CS 323, after you take CS 320. A strong theory background will help a lot in your ability to understand the literature relevant to our project, and will also help a lot in preparing you for grad school. Likewise, if you are an M.A. student under the old system, please consider taking CS 722 as well as CS 721.

Other courses that would be helpful to take, but not as essential as the above theory courses:

• A software design course. For M.A. students, this means CS 701 or equivalent. For undergrads, this means CS 309, which will be offered in fall 2001. (Note that electives are not offered every semester, so you should grab your chance to take it now, if you've fulfilled the prerequisites.)
• At least one hardware course, e.g. CS 341 (which has CS 241 as a prerequisite) or 642.

It would also be desirable for you to have some familiarity with formal methods. (If you're not already familiar with formal methods, please do get familiar with them by attending our preliminary discussions this summer.) Other big plusses would be (1) familiarity with multiple programming languages and (2) a strong math background, especially in logic and set theory.

Other factors being equal, I prefer my own former Computer Science 195 students. If you managed to do well in CS 195, then I know that you are accustomed to working hard. However, other students will be considered if they are exceptionally well qualified. Exceptionally well qualified means a GPA of at least 3.5 plus at least a majority of the above-listed qualifcations.

If one of your major aims is to gain programming experience, then you should probably wait with getting actively involved in our project until sometime in 2002. At the beginning, we will just be investigating the already-existing tools, not developing anything new. However, if possible, you should still attend the preliminary discussions that will be held this summer -- so that, when you eventually do get involved, you will already know what the project basically all about.

If you work on the project for academic credit, Dr. Shankar will be the one responsible for giving you your grade. However, you will need to register for it here at Queens College.

E-mail me (D. Nixon at dorothynixon@mindspring.com) for more details. When you write to me, please be sure to include "Research project" on the SUBJECT line of your message. In the body of your message, be sure to include your name (as known to the Registrar's Office), your student ID number, and your qualifications, including which computer science courses you have taken so far, both here at Queens College and elsewhere, including this semester (spring 2001), and your grades for courses taken in previous semesters.

Back to:

• CS 195 course website
• D. Nixon's home page