Tearing based automatic abstraction for CTL model checking

Based Automatic Abstraction for CTL Model Checking Woohyuk Lee Abelardo Pardo Jae-Young Jang Gary Hachtel Fabio Somenzi University of Colorado ECEN Campus Box 425 Boulder, CO, 80309 In this paper we present the tearing paradigm as a way to cally abstract behavior to obtain upper and lower bound approximations of a reactive system. We present algorithms that exploit the bounds to perform conservative ECTL and ACTL model checking. We also give an algorithm for false negative (or false positive) resolution for verication based on a theory of a lattice of approximations. We show that there exists a bipartition of the lattice set based on positive versus negative verication results. Our resolution methods are based on determining a pseudo-optimal shortest path from a given, possibly coarse but tractable approximation, to a nearest point on the contour separating one set of the bipartition from the other.

• Type: Conference
• Year: 1996
• Where: ICCAD
• Authors: Woohyuk Lee, Abelardo Pardo, Jae-Young Jang, Gary D. Hachtel, Fabio Somenzi
• Keywords: Hardware, ICCAD 1996, Model Checking, Negative Veri Cation, Veri Cation