Why Waste a Perfectly Good Abstraction?

@incollection{citeulike:3042547, 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.}, author = {Gurfinkel, Arie and Chechik, Marsha }, citeulike-article-id = {3042547}, doi = {http://dx.doi.org/10.1007/11691372\_14}, journal = {Tools and Algorithms for the Construction and Analysis of Systems}, keywords = {model\_checking}, pages = {212--226}, posted-at = {2008-07-25 13:09:16}, priority = {2}, title = {Why Waste a Perfectly Good Abstraction?}, url = {http://dx.doi.org/10.1007/11691372\_14}, year = {2006} }

TY - CHAP ID - citeulike:3042547 L3 - citeulike-article-id:3042547 TI - Why Waste a Perfectly Good Abstraction? JF - Tools and Algorithms for the Construction and Analysis of Systems SP - 212 EP - 226 N2 - 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. KW - model_checking AU - Gurfinkel, Arie AU - Chechik, Marsha PY - 2006/// UR - http://dx.doi.org/10.1007/11691372_14 ER -