University of Minnesota
Software Engineering Center

You are here

On the Advantages of Approximate vs. Complete Verification: Bigger Models, Faster, Less Memory, Usually Accurate.

Date of Publication: 
December 2003
Associated Research Groups: 
As software grows increasingly complex, verification becomes more and more challenging. Automatic verification by model checking has been effective in many domains including computer hardware design, networking, security and telecommunications protocols, automated control systems and others. Many realworld software models, however, are too large for the available tools. The difficulty--how to verify large systems--is fundamentally a search issue: the global state space representing all possible behaviors of a complex software system is exponential in size. This state space explosion problem has yet to be solved, even after many decades of work. We have been exploring LURCH, an approximate (not necessarily complete) alternative to traditional model checking based on a randomized search algorithm. Randomized algorithms like LURCH have been known to outperform their deterministic counterparts for search problems representing a wide range of applications.
Proceedings of the 28th Annual IEEE/NASA Software Engineering Workshop -- SEW-03. Greenbelt, Maryland, December 2003.