"During the past decade I was surprised to learn that the writing of programs for TeX and Metafont proved to be much more difficult than all the other things I had done (like proving theorems or writing books). The creation of good software demands a significantly higher standard of accuracy than those other things do, and it requires a longer attention span than other intellectual tasks. "

-Donald Knuth, Winner of the Turing Award and the National Medal of Technology.
Inventor of TeX, and author of The Art of Computer Programming

"The standard of correctness and completeness necessary to get a computer program to work at all is a couple of orders of magnitude higher than the mathematical communities standard of valid proofs. Nevertheless, large computer programs, even when they have been very carefully written and very carefully tested, always seem to have bugs."

- William P. Thurston, "On Proof and Progress in Mathematics," Bulletin of the American Math. Society

"... software verification, this 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 actual proof about the software and how it works in order to guarantee the reliability."

-Bill Gates Keynote address at WinHec 2002, talking about the SLAM project

Many aspects of our lives depend critically on software systems. As a result, research on tools, algorithms and methodologies for verifying the correctness of or finding bugs in software has become a hot area from a practical as well as theoretical standpoint. Software verification is the application of mathematical and logic-based techniques to real-life programs. Research in this area builds as much on analytical and mathematical skills as it does on disciplined programming and algorithmic skills.

Our current focus in this area is refinement verification of concurrent systems, particularly by runtime checking. We are applying our techniques on the Boxwood project, whose goal is to explore the utility of data structures and abstractions as storage infrastructure.

Recent work:

Serdar Tasiran, Shaz Qadeer
Runtime Refinement Checking of Concurrent Data Structures (Presentation slides)
In Proc. RV'04 - Fourth Workshop on Runtime Verification, April 3, 2004, Barcelona, Spain
The European Joint Conferences on Theory and Practice of Software (ETAPS '04)

Return to the Center for Advanced Design Technologies page