Automatically validating temporal safety properties of interfaces

@incollection{citeulike:2868652, abstract = {We present a process for validating temporal safety properties of software that uses a well-defined interface. The process requires only that the user state the property of interest. It then automatically creates abstractions of C code using iterative refinement, based on the given property. The process is realized in the SLAM toolkit, which consists of a model checker, predicate abstraction tool and predicate discovery tool. We have applied the SLAM toolkit to a number of Windows NT device drivers to validate critical safety properties such as correct locking behavior. We have found that the process converges on a set of predicates powerful enough to validate properties in just a few iterations.}, author = {Ball, Thomas and Rajamani, Sriram }, citeulike-article-id = {2868652}, doi = {http://dx.doi.org/10.1007/3-540-45139-0\_7}, journal = {Model Checking Software}, keywords = {2001, blast, modelchecking, read, slam, verification}, pages = {102--122}, posted-at = {2008-06-06 08:12:13}, priority = {0}, title = {Automatically validating temporal safety properties of interfaces}, url = {http://dx.doi.org/10.1007/3-540-45139-0\_7}, year = {2001} }

TY - CHAP ID - citeulike:2868652 L3 - citeulike-article-id:2868652 TI - Automatically validating temporal safety properties of interfaces JF - Model Checking Software SP - 102 EP - 122 N2 - We present a process for validating temporal safety properties of software that uses a well-defined interface. The process requires only that the user state the property of interest. It then automatically creates abstractions of C code using iterative refinement, based on the given property. The process is realized in the SLAM toolkit, which consists of a model checker, predicate abstraction tool and predicate discovery tool. We have applied the SLAM toolkit to a number of Windows NT device drivers to validate critical safety properties such as correct locking behavior. We have found that the process converges on a set of predicates powerful enough to validate properties in just a few iterations. KW - 2001 KW - blast KW - modelchecking KW - read KW - slam KW - verification AU - Ball, Thomas AU - Rajamani, Sriram PY - 2001/// UR - http://dx.doi.org/10.1007/3-540-45139-0_7 ER -