|Description: ||"... 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 conference |
Approaches to software verification may be broadly classified as code-based and model-based. The former deals directly with the source code whereas the latter deals with a high-level model of the actual code. A number of tools have emerged in the last decade to support these two methodologies, with considerable interest in industry, e.g., Alloy, CodeSurfer, Coq, Frama-C, Isabelle, Java PathFinder, PRISM, PVS, SLAM, SPIN, and UPPAAL. (Bill Gates was referring to the SLAM tool developed at Microsoft in the above quotation.)
At UB, we have been exploring the concept of runtime verification of software systems, combining aspects of both of the above approaches. We are trying to incorporate runtime verification techniques in a state-of-the-art dynamic analysis and visualization tool for Java, called JIVE, which is available as a plug-in for the Eclipse IDE and downloadable from http://www.cse.buffalo.edu/jive.
The reading materials will be drawn from published papers, tutorials, and user manuals of the tools. They will be made available through the Piazza forum to be set up for the seminar.
Grading policy: S/U, as per department policy
Meeting Time and Place: Fridays, 4-7 pm online
1 credit - class participation + presentation
3 credits - class participation + presentation + verification project
2 credits - same as 3 credits but smaller verification project
|Notes: ||This seminar is devoted to the study of concepts, methodologies, and tools for rigorous software verification. The benefits of a rigorous approach are early error detection, increased programmer productivity and software reliability. Such an approach is today seen as necessary in developing safety-critical systems where software failure can have catastrophic results. Examples include avionics systems, autonomous vehicles, medical devices, and industrial automation. |