Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software Export

@incollection{citeulike:2436600, abstract = {The Bandera Tool Set is an integrated collection of program analysis, transformation, and visualization components designed to facilitate experimentation with model-checking Java source code. Bandera takes as input Java source code and a software requirement formalized in Bandera's temporal specification language, and it generates a program model and specification in the input language of one of several existing model-checking tools (including Spin [16], dSpin [6], SMV [3], and JPF [2]). Both program slicing and user extensible abstract interpretation components are applied to customize the program model to the property being checked. When a model-checker produces an error trail, Bandera renders the error trail at the source code level and allows the user to step through the code along the path of the trail while displaying values of variables and internal states of Java lock objects.}, author = {Hatcliff, John and Dwyer, Matthew}, citeulike-article-id = {2436600}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/3-540-44685-0_5}, citeulike-linkout-1 = {http://www.springerlink.com/content/pdnkvfxdv9127n3v}, doi = {10.1007/3-540-44685-0_5}, journal = {CONCUR 2001 — Concurrency Theory}, keywords = {2001, bandera, concurrent, java, modelchecking, read, verification}, pages = {39--58}, posted-at = {2009-02-02 06:35:18}, priority = {0}, title = {Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software}, url = {http://dx.doi.org/10.1007/3-540-44685-0_5}, year = {2001} }

TY - CHAP ID - citeulike:2436600 L3 - citeulike-article-id:2436600 N2 - The Bandera Tool Set is an integrated collection of program analysis, transformation, and visualization components designed to facilitate experimentation with model-checking Java source code. Bandera takes as input Java source code and a software requirement formalized in Bandera’s temporal specification language, and it generates a program model and specification in the input language of one of several existing model-checking tools (including Spin [16], dSpin [6], SMV [3], and JPF [2]). Both program slicing and user extensible abstract interpretation components are applied to customize the program model to the property being checked. When a model-checker produces an error trail, Bandera renders the error trail at the source code level and allows the user to step through the code along the path of the trail while displaying values of variables and internal states of Java lock objects. JF - CONCUR 2001 — Concurrency Theory EP - 58 TI - Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software SP - 39 KW - 2001 KW - bandera KW - concurrent KW - java KW - modelchecking KW - read KW - verification AU - Hatcliff, John AU - Dwyer, Matthew PY - 2001/// UR - http://dx.doi.org/10.1007/3-540-44685-0_5 ER -