{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T04:07:42Z","timestamp":1746072462043,"version":"3.40.4"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2013,4,11]],"date-time":"2013-04-11T00:00:00Z","timestamp":1365638400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1007\/s10009-013-0274-1","type":"journal-article","created":{"date-parts":[[2013,4,10]],"date-time":"2013-04-10T06:55:07Z","timestamp":1365576907000},"page":"321-336","source":"Crossref","is-referenced-by-count":8,"title":["Static analysis for concurrent programs with applications to data race detection"],"prefix":"10.1007","volume":"15","author":[{"given":"Vineet","family":"Kahlon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,4,11]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of recursive state machines. In: ACM TOPLAS (2005)","key":"274_CR1","DOI":"10.1145\/1075382.1075387"},{"doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Touili, T.: On the reachability analysis of acyclic networks of pushdown systems. In: CONCUR, Lecture Notes in Computer Science, vol. 5201, pp. 356\u2013371. Springer, Heidelberg (2008)","key":"274_CR2","DOI":"10.1007\/978-3-540-85361-9_29"},{"doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software (invited chapter). In: In the Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones. LNCS, vol. 2566, pp. 85\u2013108. Springer, Heidelberg (2005)","key":"274_CR3","DOI":"10.1007\/3-540-36377-7_5"},{"doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: CONCUR. LNCS, vol. 1243, pp. 135\u2013150 (1997)","key":"274_CR4","DOI":"10.1007\/3-540-63141-0_10"},{"doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Fratani, S., Qadeer, S.: Context-bounded analysis of multithreaded programs with dynamic linked structures. In: CAV. Lecture Notes in Computer Science, vol. 4590, pp. 207\u2013 220. Springer, Heidelberg (2007)","key":"274_CR5","DOI":"10.1007\/978-3-540-73368-3_24"},{"unstructured":"Brat, G., Havelund, K., Park, S., Visser, W.: Model checking programs. In: ASE (2000)","key":"274_CR6"},{"doi-asserted-by":"crossref","unstructured":"Chugh, R., Voung, J.W., Jhala, R., Lerner, S.: Dataflow analysis for concurrent programs using datarace detection. In: PLDI, pp. 316\u2013326 (2008)","key":"274_CR7","DOI":"10.1145\/1379022.1375620"},{"doi-asserted-by":"crossref","unstructured":"Clarke, E., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on Logics of Programs, pp. 52\u201371 (1981)","key":"274_CR8","DOI":"10.1007\/BFb0025774"},{"doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, Robby, C., Zheng, H.: Bandera: Extracting finite-state models from java source code. In: ICSE (2000)","key":"274_CR9","DOI":"10.1145\/337180.337234"},{"unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming (1976)","key":"274_CR10"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","key":"274_CR11","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to Abstract interpretation, invited paper. In: PLILP\u201992. LNCS, vol. 631, pp. 269\u2013295. Springer, Heidelberg (1992)","key":"274_CR12","DOI":"10.1007\/3-540-55844-6_142"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: ACM POPL, pp. 84\u201397 (1978)","key":"274_CR13","DOI":"10.1145\/512760.512770"},{"doi-asserted-by":"crossref","unstructured":"Engler, D., Ashcraft, K.: RacerX: Effective. Static Detection of Race Conditions and Deadlocks, In: SOSP (2003)","key":"274_CR14","DOI":"10.1145\/945445.945468"},{"doi-asserted-by":"crossref","unstructured":"Farzan, A., Madhusudan, P.: Causal dataflow analysis for concurrent programs. In: TACAS. Lecture Notes in Computer Science, vol. 4424, pp. 102\u2013116. Springer, Heidelberg (2007)","key":"274_CR15","DOI":"10.1007\/978-3-540-71209-1_10"},{"doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. LNCS, vol. 1032. Springer-Verlag, Heidelberg (1996)","key":"274_CR16","DOI":"10.1007\/3-540-60761-7"},{"doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In; PLDI, pp. 266\u2013277 (2007)","key":"274_CR17","DOI":"10.1145\/1273442.1250765"},{"key":"274_CR18","volume-title":"Flow analysis for computer programs","author":"MS Hecht","year":"1977","unstructured":"Hecht, M.S.: Flow analysis for computer programs. Elsevier, North-Holland (1977)"},{"doi-asserted-by":"crossref","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: F-Soft: Software verification platform. In: CAV. LNCS, vol. 3576, pp. 301\u2013306. Springer, Heidelberg (2005)","key":"274_CR19","DOI":"10.1007\/11513988_31"},{"unstructured":"Corbett, J., Lee, K., Loginov, A., O\u2019Callahan, R., Sarkar, V., Sridharan, M.: Efficient and precise datarace detection for multithreaded object-oriented programs. In: PLDI (2002)","key":"274_CR20"},{"doi-asserted-by":"crossref","unstructured":"Kahlon, V.: Bootstrapping: A Technique for Scalable Flow and Context- Sensitive Pointer Alias Analysis. In: PLDI (2008)","key":"274_CR21","DOI":"10.1145\/1375581.1375613"},{"unstructured":"Kahlon, V.: Exploiting Program Structure for Tractable Dataflow Analysis of Concurrent Programs, draft, available upon request (kahlon@nec-labs.com)(2008)","key":"274_CR22"},{"doi-asserted-by":"crossref","unstructured":"Kahlon, V.: Boundedness vs Unboundedness of Lock Chains: Characterizing Decidability of CFL-Reachability for Threads Interacting via Locks. In: LICS (2009)","key":"274_CR23","DOI":"10.1109\/LICS.2009.45"},{"doi-asserted-by":"crossref","unstructured":"Kahlon, V., Gupta, A.: An Automata-Theoretic Approach for Model Checking Threads for LTL Properties. In: LICS (2006)","key":"274_CR24","DOI":"10.1109\/LICS.2006.11"},{"doi-asserted-by":"crossref","unstructured":"Kahlon, V., Gupta, A., Sinha, N.: Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In: CAV. Lecture Notes in Computer Science, vol. 4144, pp. 286\u2013299. Springer, Heidelberg (2006)","key":"274_CR25","DOI":"10.1007\/11817963_28"},{"doi-asserted-by":"crossref","unstructured":"Kahlon, V., Ivan\u010di\u0107, F., Gupta, A.: Reasoning about threads communicating via locks. In: CAV (2005)","key":"274_CR26","DOI":"10.1007\/11513988_49"},{"doi-asserted-by":"crossref","unstructured":"Kahlon, V., Sankaranarayanan, S., Gupta, A.: Semantic reduction of thread interleavings in concurrent programs. In: TACAS. Lecture Notes in Computer Science, vol. 5505, pp. 124\u2013138 (2009)","key":"274_CR27","DOI":"10.1007\/978-3-642-00768-2_12"},{"doi-asserted-by":"crossref","unstructured":"Kahlon, V., Yang, Y., Sankaranarayan, S., Gupta, A.: Fast and Accurate Static Data-Race Detection for Concurrent Programs. In: CAV (2007)","key":"274_CR28","DOI":"10.1007\/978-3-540-73368-3_26"},{"doi-asserted-by":"crossref","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. In: CAV. Lecture Notes in Computer Science,vol. 5123, pp. 37\u201351. Springer, Heidelberg (2008)","key":"274_CR29","DOI":"10.1007\/978-3-540-70545-1_7"},{"doi-asserted-by":"crossref","unstructured":"Lal, A., Touili, T., Kidd, N., Reps, T.W.: Interprocedural analysis of concurrent programs under a context bound. In: TACAS. Lecture Notes in Computer Science, vol. 4963, pp. 282\u2013298. Springer, Heidelberg (2008)","key":"274_CR30","DOI":"10.1007\/978-3-540-78800-3_20"},{"key":"274_CR31","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1145\/161494.161501","volume":"4","author":"W Landi","year":"1992","unstructured":"Landi, W.: Undecidability of static analysis. ACM Lett. Program. Lang. Syst. 1 4, 323\u2013337 (1992)","journal-title":"ACM Lett. Program. Lang. Syst. 1"},{"doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: PADO II. LNCS, vol. 2053, pp. 155\u2013172. Springer, Heidelberg (2001)","key":"274_CR32","DOI":"10.1007\/3-540-44978-7_10"},{"doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Fair stateless model checking. In: PLDI, pp. 362\u2013371. ACM, New York (2008)","key":"274_CR33","DOI":"10.1145\/1379022.1375625"},{"doi-asserted-by":"crossref","unstructured":"Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: POPL (2007)","key":"274_CR34","DOI":"10.1145\/1190216.1190265"},{"doi-asserted-by":"crossref","unstructured":"Naik, M., Aiken, A., Whaley, J.: Effective static race detection for java. In: PLDI (2006)","key":"274_CR35","DOI":"10.1145\/1133981.1134018"},{"doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)","key":"274_CR36","DOI":"10.1007\/978-3-662-03811-6"},{"doi-asserted-by":"crossref","unstructured":"Pratikakis, P., Foster, J.S., Hicks, M.: LOCKSMITH: Context-Sensitive Correlation Analysis for Race Detection. In: PLDI (2006)","key":"274_CR37","DOI":"10.1145\/1133981.1134019"},{"doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: TACAS (2005)","key":"274_CR38","DOI":"10.1007\/978-3-540-31980-1_7"},{"issue":"2","key":"274_CR39","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416\u2013430 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"doi-asserted-by":"crossref","unstructured":"Reps, T. W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: POPL, pp. 49\u201361 (1985)","key":"274_CR40","DOI":"10.1145\/199448.199462"},{"doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Ivan\u010di\u0107, F., Gupta, A.: Program analysis using symbolic ranges. In: SAS. LNCS, vol. 4634, pp. 366\u2013383 (2007)","key":"274_CR41","DOI":"10.1007\/978-3-540-74061-2_23"},{"doi-asserted-by":"crossref","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programming. In: ACM TCS, vol. 15(4) (1997)","key":"274_CR42","DOI":"10.1145\/265924.265927"},{"unstructured":"Sterling, N.: Warlock: A static data race analysis tool. In: USENIX Winter Technical Conference (1993)","key":"274_CR43"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0274-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0274-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0274-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T03:56:40Z","timestamp":1745985400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0274-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,11]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["274"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0274-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2013,4,11]]}}}