Why waste a perfectly good abstraction?

Abstract

Software model-checking based on the CEGAR framework can be made more precise by separating non-determinism from the lack of information due to abstraction. The two can be modeled individually using four-valued Belnap logic. In addition, this logic allows reasoning about negations effectively and thus enables checking of full CTL. In this paper, we present YASM - a new symbolic software model-checker. Preliminary experience with YASM shows that our implementation can effectively construct and analyze Belnap models without a substantial overhead when compared to its classical counterparts. © Springer-Verlag Berlin Heidelberg 2006.