Adapting side effects analysis for modular program model checking Export

@article{citeulike:4012227, abstract = {There is a widely held belief that whole program analysis is intractable for large complex software systems, and there can be little doubt that this is true for program analyses based on model checking. Model checking selected program components that comprise a cohesive unit, however, can be an effective way of uncovering subtle coding errors, especially for components of multi-threaded programs. In this setting, one of the chief problems is how to safely approximate the behavior of the rest of the application as it relates to the unit being analyzed.Non-unit application components are collectively referred to as the environment. In this paper, we describe how points-to and side-effects analyses can be adapted to support generation of summaries of environment behavior that can be reified into Java code using special modeling primitives. The resulting abstract models of the environment can be combined with the code of the unit and then model checked against unit properties. We present our analysis framework, illustrate its flexibility in generating several types of models, and present experience that provides evidence of the scalability of the approach.}, address = {New York, NY, USA}, author = {Tkachuk, Oksana and Dwyer, Matthew B.}, citeulike-article-id = {4012227}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=949952.940097}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/949952.940097}, doi = {10.1145/949952.940097}, issn = {0163-5948}, journal = {SIGSOFT Softw. Eng. Notes}, keywords = {2003, analysis, bandera, modelchecking, tool}, number = {5}, pages = {188--197}, posted-at = {2009-02-05 14:21:26}, priority = {2}, publisher = {ACM}, title = {Adapting side effects analysis for modular program model checking}, url = {http://dx.doi.org/10.1145/949952.940097}, volume = {28}, year = {2003} }

TY - JOUR ID - citeulike:4012227 L3 - citeulike-article-id:4012227 N2 - There is a widely held belief that whole program analysis is intractable for large complex software systems, and there can be little doubt that this is true for program analyses based on model checking. Model checking selected program components that comprise a cohesive unit, however, can be an effective way of uncovering subtle coding errors, especially for components of multi-threaded programs. In this setting, one of the chief problems is how to safely approximate the behavior of the rest of the application as it relates to the unit being analyzed.Non-unit application components are collectively referred to as the environment. In this paper, we describe how points-to and side-effects analyses can be adapted to support generation of summaries of environment behavior that can be reified into Java code using special modeling primitives. The resulting abstract models of the environment can be combined with the code of the unit and then model checked against unit properties. We present our analysis framework, illustrate its flexibility in generating several types of models, and present experience that provides evidence of the scalability of the approach. IS - 5 JF - SIGSOFT Softw. Eng. Notes SN - 0163-5948 AD - New York, NY, USA EP - 197 TI - Adapting side effects analysis for modular program model checking PB - ACM VL - 28 SP - 188 KW - 2003 KW - analysis KW - bandera KW - modelchecking KW - tool AU - Tkachuk, Oksana AU - Dwyer, Matthew PY - 2003/// UR - http://dx.doi.org/10.1145/949952.940097 ER -