Exploring very large state spaces using genetic algorithms

Patrice Godefroid and Sarfraz Khurshid

From the issue entitled "Special section on tools and algorithms for the construction and analysis of systems"

View Related Documents

Abstract

We present a novel framework for exploring very large state spaces of concurrent reactive systems. Our framework exploits application-independent heuristics using genetic algorithms to guide a state-space search toward error states. We have implemented this framework in conjunction with VeriSoft, a tool for exploring the state spaces of software applications composed of several concurrent processes executing arbitrary code. We present experimental results obtained with several examples of programs, including a C implementation of a public-key authentication protocol. We discuss heuristics and properties of state spaces that help a genetic search detect deadlocks and assertion violations. For finding errors in very large state spaces, our experiments show that a genetic search using simple heuristics can significantly outperform random and systematic searches.

Keywords  Model checking - Verification - State-space exploration - Heuristics - Genetic algorithms

Fulltext Preview

Image of the first page of the fulltext document