Software Model Checking

Authored by: Alastair Donaldson

Computing Handbook

Print publication date:  May  2014
Online publication date:  May  2014

Print ISBN: 9781439898529
eBook ISBN: 9781439898536
Adobe ISBN:


 Download Chapter



This chapter provides an overview of techniques and tools for analyzing the correctness of software systems using model checking. After providing some background on traditional finite-state model checking and related tools (Section 89.2, we give an overview of two classes of techniques that have allowed model checking to be applied directly to the source code of large software systems: counterexample-guided abstraction refinement (CEGAR) using predicate abstraction (Section 89.3), and bounded model checking (Section 89.4). The chapter concludes with a brief survey of tools that leverage traditional model checking methods for the analysis of software systems (Section 89.5). Software model checking techniques based on CEGAR and bounded model checking are also treated in the Software Verification chapter of the Handbook of Satisfiability [73]; we believe these chapters complement one another.

Search for more...
Back to top

Use of cookies on this website

We are using cookies to provide statistics that help us give you the best experience of our site. You can find out more in our Privacy Policy. By continuing to use the site you are agreeing to our use of cookies.