Instructor: Dr. Bharat Jayaraman
"... software verification has been the holy grail of computer science for many decades, but now in some very key areas, for example, driver verification, we're building tools that can do an actual proof about the software and how it works in order to guarantee reliability." - Bill Gates, keynote address, WinHEC 2002 conference
This seminar is devoted to the study of concepts, methodologies, and tools for rigorous software development. The benefits of a rigorous approach are early error detection, increased programmer productivity, and more reliable software. Towards this end, a number of tools have emerged in the last decade and are being adopted in industry, for example, Code Contracts, CodeSurfer, Coverity, Java PathFinder, SLAM, and SPIN. (Bill Gates was referring to the SLAM tool developed at Microsoft in the above quotation.)
The abovementioned tools are based upon static as well as dynamic analysis techniques, such as data-flow analysis, program slicing, model checking, abstract interpretation, symbolic execution, test-case generation, and verification. At UB, we have been developing a state-of-the-art dynamic analysis and visualization tool for Java, called JIVE, which is available as an Eclipse plug-in and has been used at the graduate and undergraduate levels.
The instructor will provide an introduction to the concepts underlying the tools in order to make the seminar self-contained. Thus, any CSE graduate student could potentially take the seminar. The reading materials will be drawn from published papers, tutorials, and user manuals of the tools.
Prerequisites: Graduate Standing in CSE
Grading policy: S/U, as per department policy
Meeting Time and Place: Fridays, 4-6 pm in Davis 113A
Course requirements: Class Attendance and Participation. Additionally:
Please email the instructor, Dr. Bharat Jayaraman (bharat@buffalo.edu), if you are interested in taking the seminar for credit.