Sagar Chaki

Sagar Chaki, Arie Gurfinkel, Chapter of the Handbook of Model Checking (HBMC).

Abstract: Symbolic model checking based on Binary Decision Diagrams (BDDs) is one of the most celebrated breakthroughs in the area of formal verification. It was originally proposed in the context of hardware model checking, and advanced the state of the art in model-checking capability by several orders of magnitude in terms of the sizes of state spaces that could be explored successfully. More recently, it has been extended to the domain of software verification as well, and several BDD-based model checkers for Boolean programs and push-down systems have been developed. In this chapter, we summarize some of the key concepts and techniques that have emerged in this story of successful practical verification.