{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:43Z","timestamp":1751660503346},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288715"},{"type":"electronic","value":"9783642288722"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28872-2_25","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:48:16Z","timestamp":1332449296000},"page":"362-376","source":"Crossref","is-referenced-by-count":14,"title":["Language-Theoretic Abstraction Refinement"],"prefix":"10.1007","author":[{"given":"Zhenyue","family":"Long","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georgel","family":"Calin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"Armstrong, J., Virding, R., Wikstr\u00f6m, C., Williams, M.: Concurrent Programming in Erlang, 2nd edn. Prentice Hall (1996)"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL 2002: Principles of Programming Languages, pp. 1\u20133. ACM (2002)","DOI":"10.1145\/565816.503274"},{"issue":"4","key":"25_CR3","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1142\/S0129054103001893","volume":"14","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. International Journal on Foundations of Computer Science\u00a014(4), 551\u2013582 (2003)","journal-title":"International Journal on Foundations of Computer Science"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/11691372_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Chaki","year":"2006","unstructured":"Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying Concurrent Message-Passing C Programs with Recursive Calls. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 334\u2013349. Springer, Heidelberg (2006)"},{"issue":"5","key":"25_CR5","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-78800-3_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2008","unstructured":"Clarke, E.M., Talupur, M., Veith, H.: Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 33\u201347. Springer, Heidelberg (2008)"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-02737-6_16","volume-title":"Developments in Language Theory","author":"\u00d6. E\u011fecio\u011flu","year":"2009","unstructured":"E\u011fecio\u011flu, \u00d6.: Strongly Regular Grammars and Regular Approximation of Context-Free Languages. In: Diekert, V., Nowotka, D. (eds.) DLT 2009. LNCS, vol.\u00a05583, pp. 207\u2013220. Springer, Heidelberg (2009)"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ganty, P.: Complexity of pattern-based verification for multithreaded programs. In: POPL 2011: Principles of Programming Languages, pp. 499\u2013510. ACM (2011)","DOI":"10.1145\/1925844.1926443"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/978-3-642-14295-6_52","volume-title":"Computer Aided Verification","author":"P. Ganty","year":"2010","unstructured":"Ganty, P., Majumdar, R., Monmege, B.: Bounded Underapproximations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 600\u2013614. Springer, Heidelberg (2010)"},{"issue":"2","key":"25_CR10","first-page":"333","volume":"113","author":"S. Ginsburg","year":"1964","unstructured":"Ginsburg, S., Spanier, E.H.: Bounded Algol-like languages. Transactions of the American Mathematical Society\u00a0113(2), 333\u2013368 (1964)","journal-title":"Transactions of the American Mathematical Society"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL 2011: Principles of Programming Languages, pp. 331\u2013344. ACM (2011)","DOI":"10.1145\/1925844.1926424"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: PLDI 2004: Programming Language Design and Implementation, pp. 1\u201313. ACM (2004)","DOI":"10.1145\/996841.996844"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-Modular Abstraction Refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 262\u2013274. Springer, Heidelberg (2003)"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002: Principles of Programming Languages, pp. 58\u201370. ACM (2002)","DOI":"10.1145\/565816.503279"},{"key":"25_CR15","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979)"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Kahlon, V.: Boundedness vs. unboundedness of lock chains: Characterizing decidability of pairwise CFL-reachability for threads communicating via locks. In: LICS 2009: Logic in Computer Science, pp. 27\u201336. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.45"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Gupta, A.: On the analysis of interacting pushdown systems. In: POPL 2003: Principles of Programming Languages, pp. 303\u2013314. ACM (2007)","DOI":"10.1145\/1190215.1190262"},{"key":"25_CR18","unstructured":"Kidd, N.: Bluetooth protocol, \n                    \n                      http:\/\/pages.cs.wisc.edu\/~kidd\/bluetooth\/"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-70545-1_7","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2008","unstructured":"Lal, A., Reps, T.: Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 37\u201351. Springer, Heidelberg (2008)"},{"key":"25_CR20","unstructured":"Latteux, M., Leguy, J.: Une propri\u00e9t\u00e9 de la famille GRE. In: FCT 1979, pp. 255\u2013261. Akademie-Verlag (1979)"},{"key":"25_CR21","unstructured":"Mohri, M., Nederhof, M.-J.: Regular approximation of context-free grammars through transformation. In: Robustness in Language and Speech Technology, vol.\u00a09, pp. 251\u2013261. Kluwer Academic Publishers (2000)"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-540-73368-3_28","volume-title":"Computer Aided Verification","author":"G. Patin","year":"2007","unstructured":"Patin, G., Sighireanu, M., Touili, T.: Spade: Verification of Multithreaded Dynamic and Recursive Programs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 254\u2013257. Springer, Heidelberg (2007)"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-Bounded Model Checking of Concurrent Software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: Kiss: keep it simple and sequential. In: PLDI 2004: Programming Language Design and Implementation, pp. 14\u201324. ACM (2004)","DOI":"10.1145\/996841.996845"},{"key":"25_CR25","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.entcs.2009.05.036","volume":"239","author":"N. Ben Rajeb","year":"2009","unstructured":"Ben Rajeb, N., Nasraoui, B., Robbana, R., Touili, T.: Verifying multithreaded recursive programs with integer variables. Electr. Notes Theor. Comput. Sci.\u00a0239, 143\u2013154 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"2","key":"25_CR26","doi-asserted-by":"publisher","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 TOPLAS\u00a022(2), 416\u2013430 (2000)","journal-title":"ACM TOPLAS"},{"key":"25_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-540-85114-1_19","volume-title":"Model Checking Software","author":"D. Suwimonteerabuth","year":"2008","unstructured":"Suwimonteerabuth, D., Esparza, J., Schwoon, S.: Symbolic Context-Bounded Analysis of Multithreaded Java Programs. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol.\u00a05156, pp. 270\u2013287. Springer, Heidelberg (2008)"},{"issue":"3","key":"25_CR28","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/0012-365X(78)90156-5","volume":"21","author":"J. Leeuwen van","year":"1978","unstructured":"van Leeuwen, J.: Effective constructions in well-partially-ordered free monoids. Discrete Mathematics\u00a021(3), 237\u2013252 (1978)","journal-title":"Discrete Mathematics"},{"issue":"12","key":"25_CR29","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"3","author":"G.L. Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett.\u00a03(12), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28872-2_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T23:57:18Z","timestamp":1556495838000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28872-2_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288715","9783642288722"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28872-2_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}