Advertisement
Published in:
2012 | OriginalPaper | Chapter
Model Checking and the State Explosion Problem
Authors : Edmund M. Clarke, William Klieber, Miloš Nováček, Paolo Zuliani
Published in: Tools for Practical Software Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Model checking is an automatic verification technique for hardware and software systems that are finite state or have finite state abstractions. It has been used successfully to verify computer hardware, and it is beginning to be used to verify computer software as well. As the number of state variables in the system increases, the size of the system state space grows exponentially. This is called the “state explosion problem”. Much of the research in model checking over the past 30 years has involved developing techniques for dealing with this problem. In these lecture notes, we will explain how the basic model checking algorithms work and describe some recent approaches to the state explosion problem, with an emphasis on Bounded Model Checking.