Boolean and Cartesian Abstraction for Model Checking C Programs Export

@article{citeulike:3464384, abstract = {The problem of model checking a specification in form of a C program with recursive procedures and many thousands of lines of code has not been addressed before. In this paper, we show how we attack this problem using an abstraction that is formalized with the Cartesian abstraction. It is implemented through a source-to-source transformation into a 'Boolean' C program; we give an algorithm to compute the transformation with a cost that is exponential in its theoretical worst-case complexity but feasible in practice.}, author = {Ball, Thomas and Podelski, Andreas and Rajamani, Sriram K.}, citeulike-article-id = {3464384}, keywords = {2000, blast, booleanprogram, modelchecking, read, slam, slide}, month = {December}, posted-at = {2008-10-30 06:43:12}, priority = {0}, title = {Boolean and Cartesian Abstraction for Model Checking C Programs}, year = {2000} }

TY - JOUR ID - citeulike:3464384 L3 - citeulike-article-id:3464384 N2 - The problem of model checking a specification in form of a C program with recursive procedures and many thousands of lines of code has not been addressed before. In this paper, we show how we attack this problem using an abstraction that is formalized with the Cartesian abstraction. It is implemented through a source-to-source transformation into a 'Boolean' C program; we give an algorithm to compute the transformation with a cost that is exponential in its theoretical worst-case complexity but feasible in practice. TI - Boolean and Cartesian Abstraction for Model Checking C Programs KW - 2000 KW - blast KW - booleanprogram KW - modelchecking KW - read KW - slam KW - slide AU - Ball, Thomas AU - Podelski, Andreas AU - Rajamani, Sriram PY - 2000/12// ER -