{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:20:11Z","timestamp":1740097211264,"version":"3.37.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319278094"},{"type":"electronic","value":"9783319278100"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-27810-0_5","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T02:38:33Z","timestamp":1450924713000},"page":"88-110","source":"Crossref","is-referenced-by-count":0,"title":["An Automata-Based Approach to Trace Partitioned Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Mads Christian","family":"Olesen","sequence":"first","affiliation":[]},{"given":"Ren\u00e9 Rydhof","family":"Hansen","sequence":"additional","affiliation":[]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","volume-title":"Computer Aided Verification","author":"R Alur","year":"1999","unstructured":"Alur, R.: Timed automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8\u201322. Springer, Heidelberg (1999)"},{"key":"5_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, New York (2008)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-540-73368-3_51","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504\u2013518. Springer, Heidelberg (2007). \n                    http:\/\/dx.doi.org\/10.1007\/978-3-540-73368-3_51"},{"issue":"5","key":"5_CR5","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Programm. Lang. Syst. (TOPLAS) 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Programm. Lang. Syst. (TOPLAS)"},{"key":"5_CR6","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: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1977), pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"issue":"3","key":"5_CR7","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10703-009-0089-6","volume":"35","author":"P Cousot","year":"2009","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Why does ASTR\u00c9E scale up? Formal Meth. Syst. Des. 35(3), 229\u2013264 (2009)","journal-title":"Formal Meth. Syst. Des."},{"key":"5_CR8","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages (POPL 1979), pp. 269\u2013282. ACM Press, San Antonio (1979). \n                    http:\/\/dblp.org\/db\/conf\/popl\/popl79.html#CousotC79"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269\u2013295. Springer, Heidelberg (1992)"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P Cousot","year":"1999","unstructured":"Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Autom. Softw. Eng. 6, 69\u201395 (1999). \n                    http:\/\/dblp.org\/db\/journals\/ase\/ase6.html#CousotC99","journal-title":"Autom. Softw. Eng."},{"key":"5_CR11","unstructured":"Dalsgaard, A.E., Hansen, R.R., J\u00f8rgensen, K.Y., Larsen, K.G., Olesen, M.C., Olsen, P., Srba, J.: opaal: a lattice model checker. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 487\u2013493. Springer, Heidelberg (2011). \n                    http:\/\/dblp.org\/db\/conf\/nfm\/nfm2011.html#DalsgaardHJLOOS11"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-33365-1_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"AE Dalsgaard","year":"2012","unstructured":"Dalsgaard, A.E., Laarman, A., Larsen, K.G., Olesen, M.C., van de Pol, J.: Multi-core reachability for timed automata. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 91\u2013106. Springer, Heidelberg (2012). \n                    http:\/\/dblp.org\/db\/conf\/formats\/formats2012.html#DalsgaardLLOP12"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/BFb0054180","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Daws","year":"1998","unstructured":"Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313\u2013329. Springer, Heidelberg (1998)"},{"issue":"1\u20132","key":"5_CR14","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"5_CR15","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1016\/j.jcss.2005.09.001","volume":"72","author":"G Geeraerts","year":"2006","unstructured":"Geeraerts, G., Raskin, J.F., Van Begin, L.: Expand, enlarge and check: new algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180 (2006)","journal-title":"J. Comput. Syst. Sci."},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-540-74061-2_22","volume-title":"Static Analysis","author":"D Gopan","year":"2007","unstructured":"Gopan, D., Reps, T.: Guided static analysis. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 349\u2013365. Springer, Heidelberg (2007). \n                    http:\/\/dl.acm.org\/citation.cfm?id=2391451.2391475"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-49727-7_12","volume-title":"Static Analysis","author":"M Handjieva","year":"1998","unstructured":"Handjieva, M., Tzolovski, S.: Refining static analyses by trace-based partitioning using control flow. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 200\u2013214. Springer, Heidelberg (1998). \n                    http:\/\/dblp.org\/db\/conf\/sas\/sas98.html#HandjievaT98"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002), pp. 58\u201370. ACM (2002)","DOI":"10.1145\/565816.503279"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-48294-6_3","volume-title":"Static Analysis","author":"B Jeannet","year":"1999","unstructured":"Jeannet, B., Halbwachs, N., Raymond, P.: Dynamic partitioning in analyses of numerical properties. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 39\u201350. Springer, Heidelberg (1999). \n                    http:\/\/dblp.org\/db\/conf\/sas\/sas99.html#JeannetHR99"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). \n                    http:\/\/dblp.org\/db\/conf\/sas\/sas99.html#JeannetHR99"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-69738-1_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"O Kupferman","year":"2007","unstructured":"Kupferman, O., Lustig, Y.: Lattice automata. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 199\u2013213. Springer, Heidelberg (2007)"},{"key":"5_CR22","unstructured":"Laarman, A.: Scalable multi-core model checking. Ph.D. thesis, University of Twente (2014)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/978-3-642-20398-5_40","volume-title":"NASA Formal Methods","author":"A Laarman","year":"2011","unstructured":"Laarman, A., van de Pol, J., Weber, M.: Multi-core LTSmin: marrying modularity and scalability. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 506\u2013511. Springer, Heidelberg (2011). \n                    http:\/\/dblp.org\/db\/conf\/nfm\/nfm2011.html#LaarmanPW11"},{"issue":"1","key":"5_CR24","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer (STTT) 1(1), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer (STTT)"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"del Mar Gallardo, M., Martinez, J., Merino, P., Pimentel, E.: aSPIN: Extending SPIN with abstraction. In: Model Checking Software, pp. 241\u2013252 (2002)","DOI":"10.1007\/3-540-46017-9_24"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-31987-0_2","volume-title":"Programming Languages and Systems","author":"L Mauborgne","year":"2005","unstructured":"Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5\u201320. Springer, Heidelberg (2005)"},{"issue":"1","key":"5_CR27","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symbolic Comput. (HOSC) 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symbolic Comput. (HOSC)"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/11575467_7","volume-title":"Programming Languages and Systems","author":"D Monniaux","year":"2005","unstructured":"Monniaux, D.: The parallel implementation of the Astr\u00e9e static analyzer. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 86\u201396. Springer, Heidelberg (2005). \n                    http:\/\/dx.doi.org\/10.1007\/11575467_7"},{"key":"5_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer-Verlag New York Inc., Secaucus (1999)"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-642-12032-9_14","volume-title":"Foundations of Software Science and Computational Structures","author":"F Nielson","year":"2010","unstructured":"Nielson, F., Nielson, H.R.: Model checking Is static analysis of modal logic. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 191\u2013205. Springer, Heidelberg (2010)"},{"key":"5_CR31","unstructured":"Olesen, M.C.: Program analysis as model checking. Ph.D. thesis, Aalborg University (defended December 2013)"},{"issue":"5","key":"5_CR32","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/1275497.1275501","volume":"29","author":"X Rival","year":"2007","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. (TOPLAS) 29(5), 26 (2007). \n                    http:\/\/dblp.org\/db\/journals\/toplas\/toplas29.html#RivalM07","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","volume-title":"Static Analysis","author":"DA Schmidt","year":"1998","unstructured":"Schmidt, D.A., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 351\u2013380. Springer, Heidelberg (1998)"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-54415-1_54","volume-title":"Theoretical Aspects of Computer Software","author":"B Steffen","year":"1991","unstructured":"Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346\u2013365. Springer, Heidelberg (1991). \n                    http:\/\/dx.doi.org\/10.1007\/3-540-54415-1_54"},{"issue":"2","key":"5_CR35","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0167-6423(93)90003-8","volume":"21","author":"B Steffen","year":"1993","unstructured":"Steffen, B.: Generating data flow analysis algorithms from modal specifications. Sci. Comput. Program. 21(2), 115\u2013139 (1993). \n                    http:\/\/dx.doi.org\/10.1016\/0167-6423(93)90003-8","journal-title":"Sci. Comput. Program."},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-61739-6_31","volume-title":"Static Analysis","author":"B Steffen","year":"1996","unstructured":"Steffen, B.: Property-oriented expansion. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 22\u201341. Springer, Heidelberg (1996). \n                    http:\/\/dblp.org\/db\/conf\/sas\/sas96.html#Steffen96"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-60218-6_6","volume-title":"CONCUR \u201995 Concurrency Theory","author":"B Steffen","year":"1995","unstructured":"Steffen, B., Classen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 72\u201387. Springer, Heidelberg (1995). \n                    http:\/\/dblp.org\/db\/conf\/concur\/concur1995.#htmlSteffenCKKM95"}],"container-title":["Lecture Notes in Computer Science","Semantics, Logics, and Calculi"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-27810-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:34:57Z","timestamp":1559349297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-27810-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783319278094","9783319278100"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-27810-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015,12,25]]}}}