{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T20:34:23Z","timestamp":1760646863107,"version":"3.37.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319944593"},{"type":"electronic","value":"9783319944609"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94460-9_5","type":"book-chapter","created":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T11:36:38Z","timestamp":1531136198000},"page":"73-90","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["CARET Analysis of Multithreaded Programs"],"prefix":"10.1007","author":[{"given":"Huu-Vu","family":"Nguyen","sequence":"first","affiliation":[]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,10]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-24730-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2004","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467\u2013481. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_35"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-540-85361-9_29","volume-title":"CONCUR 2008 - Concurrency Theory","author":"MF Atig","year":"2008","unstructured":"Atig, M.F., Bouajjani, A., Touili, T.: On the reachability analysis of acyclic networks of pushdown systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 356\u2013371. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85361-9_29"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-642-02979-0_18","volume-title":"Implementation and Application of Automata","author":"MF Atig","year":"2009","unstructured":"Atig, M.F., Touili, T.: Verifying parallel programs with dynamic communication structures. In: Maneth, S. (ed.) CIAA 2009. LNCS, vol. 5642, pp. 145\u2013154. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02979-0_18"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-642-38536-0_35","volume-title":"Computer Science \u2013 Theory and Applications","author":"K Bansal","year":"2013","unstructured":"Bansal, K., Demri, S.: Model-checking bounded multi-pushdown systems. In: Bulatov, A.A., Shur, A.M. (eds.) CSR 2013. LNCS, vol. 7913, pp. 405\u2013417. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38536-0_35"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL 2003 (2003)","DOI":"10.1145\/604131.604137"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/11539452_36","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A Bouajjani","year":"2005","unstructured":"Bouajjani, A., M\u00fcller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 473\u2013487. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11539452_36"},{"key":"5_CR7","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., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 334\u2013349. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_22"},{"key":"5_CR8","unstructured":"Grumberg, O., Clarke, E.M., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-18275-4_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"TM Gawlitza","year":"2011","unstructured":"Gawlitza, T.M., Lammich, P., M\u00fcller-Olm, M., Seidl, H., Wenner, A.: Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 199\u2013213. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_15"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Gupta, A.: An automata-theoretic approach for model checking threads for LTL properties. In: LICS 2006 (2006)","DOI":"10.1109\/LICS.2006.11"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Gupta, A.: On the analysis of interacting pushdown systems. In: POPL 2007 (2007)","DOI":"10.1145\/1190216.1190262"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/11513988_49","volume-title":"Computer Aided Verification","author":"Vineet Kahlon","year":"2005","unstructured":"Kahlon, V., Ivancic, F., Gupta, A.: Reasoning about threads communicating via locks. In: CAV 2005 (2005)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-33475-7_16","volume-title":"Theoretical Computer Science","author":"S Torre La","year":"2012","unstructured":"La Torre, S., Napoli, M.: A temporal logic for multi-threaded programs. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 225\u2013239. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33475-7_16"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-642-02658-4_39","volume-title":"Computer Aided Verification","author":"P Lammich","year":"2009","unstructured":"Lammich, P., M\u00fcller-Olm, M., Wenner, A.: Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 525\u2013539. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_39"},{"issue":"4","key":"5_CR15","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1142\/S0129054111008453","volume":"22","author":"D Lugiez","year":"2011","unstructured":"Lugiez, D.: Forward analysis of dynamic network of pushdown systems is easier without order. Int. J. Found. Comput. Sci. 22(4), 843\u2013862 (2011)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Nguyen, H.-V., Touili, T.: CARET model checking for malware detection. In: SPIN 2017 (2017)","DOI":"10.1145\/3092282.3092301"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Nguyen, H.-V., Touili, T.: CARET model checking for pushdown systems. In: SAC 2017 (2017)","DOI":"10.1145\/3019612.3019829"},{"key":"5_CR18","unstructured":"Schwoon, S.: Model-checking pushdown systems. Dissertation, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen (2002)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-319-03542-0_3","volume-title":"Programming Languages and Systems","author":"F Song","year":"2013","unstructured":"Song, F., Touili, T.: Model checking dynamic pushdown networks. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 33\u201349. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03542-0_3"},{"key":"5_CR20","unstructured":"Song, F., Touili, T.: LTL model-checking for dynamic pushdown networks communicating via locks. CoRR, abs\/1611.02528 (2016)"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"590","DOI":"10.1007\/978-3-642-11957-6_31","volume-title":"Programming Languages and Systems","author":"A Wenner","year":"2010","unstructured":"Wenner, A.: Weighted dynamic pushdown networks. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 590\u2013609. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_31"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94460-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T10:22:26Z","timestamp":1571566946000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94460-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319944593","9783319944609"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94460-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}