{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:36:21Z","timestamp":1725903381545},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_11","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"166-184","source":"Crossref","is-referenced-by-count":1,"title":["Decision Procedures for Theories of Sets with Measures"],"prefix":"10.1007","author":[{"given":"Markus","family":"Bender","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viorica","family":"Sofronie-Stokkermans","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-319-40229-1_6","volume-title":"Automated Reasoning","author":"F Alberti","year":"2016","unstructured":"Alberti, F., Ghilardi, S., Pagani, E.: Counting constraints in flat array fragments. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 65\u201381. Springer, Cham (2016). doi:\n10.1007\/978-3-319-40229-1_6"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-40229-1_7","volume-title":"Automated Reasoning","author":"K Bansal","year":"2016","unstructured":"Bansal, K., Reynolds, A., Barrett, C., Tinelli, C.: A new decision procedure for finite sets and cardinality constraints in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 82\u201398. Springer, Cham (2016). doi:\n10.1007\/978-3-319-40229-1_7"},{"key":"11_CR3","unstructured":"Bender, M.: Reasoning with sets and sums of sets. In: King, T., Piskac, R. (eds.) SMT@IJCAR 2016, Proceedings. CEUR Workshop Proceedings, vol. 1617, pp. 61\u201370. CEUR-WS.org (2016)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-60045-0_51","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"1995","unstructured":"Bouajjani, A., Lakhnech, Y., Robbana, R.: From duration calculus to linear hybrid automata. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 196\u2013210. Springer, Heidelberg (1995). doi:\n10.1007\/3-540-60045-0_51"},{"key":"11_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-06784-0","volume-title":"Duration Calculus: A Formal Approach to Real-Time Systems","author":"Z Chaochen","year":"2004","unstructured":"Chaochen, Z., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. Springer, Berlin (2004)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-56503-5_8","volume-title":"STACS 93","author":"Z Chaochen","year":"1993","unstructured":"Chaochen, Z., Hansen, M.R., Sestoft, P.: Decidability and undecidability results for duration calculus. In: Enjalbert, P., Finkel, A., Wagner, K.W. (eds.) STACS 1993. LNCS, vol. 665, pp. 58\u201368. Springer, Heidelberg (1993). doi:\n10.1007\/3-540-56503-5_8"},{"issue":"5","key":"11_CR7","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z Chaochen","year":"1991","unstructured":"Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991)","journal-title":"Inf. Process. Lett."},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-57318-6_23","volume-title":"Hybrid Systems","author":"Z Chaochen","year":"1993","unstructured":"Chaochen, Z., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 36\u201359. Springer, Heidelberg (1993). doi:\n10.1007\/3-540-57318-6_23"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-45616-3_5","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"N Chetcuti-Sperandio","year":"2002","unstructured":"Chetcuti-Sperandio, N.: Tableau-based automated deduction for duration calculus. In: Egly, U., Ferm\u00fcller, C.G. (eds.) TABLEAUX 2002. LNCS, vol. 2381, pp. 53\u201369. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-45616-3_5"},{"issue":"11","key":"11_CR10","first-page":"743","volume":"5","author":"N Chetcuti-Sperandio","year":"1999","unstructured":"Chetcuti-Sperandio, N., del Cerro, L.F.: A decision method for duration calculus. J. UCS 5(11), 743\u2013764 (1999)","journal-title":"J. UCS"},{"issue":"6","key":"11_CR11","doi-asserted-by":"crossref","first-page":"877","DOI":"10.1093\/logcom\/10.6.877","volume":"10","author":"N Chetcuti-Sperandio","year":"2000","unstructured":"Chetcuti-Sperandio, N., del Cerro, L.F.: A mixed decision method for duration calculus. J. Log. Comput. 10(6), 877\u2013895 (2000)","journal-title":"J. Log. Comput."},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-08587-6_9","volume-title":"Automated Reasoning","author":"P Chocron","year":"2014","unstructured":"Chocron, P., Fontaine, P., Ringeissen, C.: A gentle non-disjoint combination of satisfiability procedures. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 122\u2013136. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08587-6_9"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-71209-1_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Hansen, M.R.: Deciding an interval logic with accumulated durations. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 201\u2013215. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-71209-1_17"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-14203-1_4","volume-title":"Automated Reasoning","author":"C Ihlemann","year":"2010","unstructured":"Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 30\u201345. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-14203-1_4"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-02658-4_29","volume-title":"Computer Aided Verification","author":"S Jacobs","year":"2009","unstructured":"Jacobs, S.: Incremental instance generation in local reasoning. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 368\u2013382. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-02658-4_29"},{"key":"11_CR16","unstructured":"Kapur, D., Zarba, C.G.: A reduction approach to decision procedures (2005). \nhttps:\/\/www.cs.unm.edu\/~kapur\/mypapers\/reduction.pdf,\n\n. Unpublished manuscript"},{"issue":"1","key":"11_CR17","first-page":"191","volume":"20","author":"L Khachiyan","year":"1979","unstructured":"Khachiyan, L.: A polynomial algorithm in linear programming. Soviet Math. Dokl. 20(1), 191\u2013194 (1979)","journal-title":"Soviet Math. Dokl."},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11532231_20","volume-title":"Automated Deduction \u2013 CADE-20","author":"V Kuncak","year":"2005","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean algebra with Presburger arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 260\u2013277. Springer, Heidelberg (2005). doi:\n10.1007\/11532231_20"},{"issue":"3","key":"11_CR19","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10817-006-9042-1","volume":"36","author":"V Kuncak","year":"2006","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.C.: Deciding Boolean algebra with Presburger arithmetic. J. Autom. Reasoning 36(3), 213\u2013239 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-15205-4_5","volume-title":"Computer Science Logic","author":"V Kuncak","year":"2010","unstructured":"Kuncak, V., Piskac, R., Suter, P.: Ordered sets in the calculus of data structures. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 34\u201348. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-15205-4_5"},{"key":"11_CR21","unstructured":"Ohlbach, H.J.: Set description languages and reasoning about numerical features of sets. In: Lambrix, P., Borgida, A., Lenzerini, M., M\u00f6ller, R., Patel-Schneider, P.F. (eds.) International Workshop on Description Logics (DL 1999), Proceedings. CEUR Workshop Proceedings, vol. 22. CEUR-WS.org (1999)"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 219\u2013234. Springer, Heidelberg (2005). doi:\n10.1007\/11532231_16"},{"issue":"4\u20136","key":"11_CR23","first-page":"397","volume":"13","author":"V Sofronie-Stokkermans","year":"2007","unstructured":"Sofronie-Stokkermans, V., Ihlemann, C.: Automated reasoning in some local extensions of ordered structures. Multiple-Valued Logic Soft Comput. 13(4\u20136), 397\u2013414 (2007)","journal-title":"Multiple-Valued Logic Soft Comput."},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-642-04222-5_23","volume-title":"Frontiers of Combining Systems","author":"T Wies","year":"2009","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 366\u2013382. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-04222-5_23"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-642-11319-2_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K Yessenov","year":"2010","unstructured":"Yessenov, K., Piskac, R., Kuncak, V.: Collections, cardinalities, and relations. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 380\u2013395. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-11319-2_27"},{"issue":"1","key":"11_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-005-3075-8","volume":"34","author":"CG Zarba","year":"2005","unstructured":"Zarba, C.G.: Combining sets with cardinals. J. Autom. Reasoning 34(1), 1\u201329 (2005)","journal-title":"J. Autom. Reasoning"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: Gupta, R., Amarasinghe, S.P. (eds.), Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, 7\u201313 June 2008, pp. 349\u2013361. ACM (2008)","DOI":"10.1145\/1375581.1375624"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/3-540-58468-4_161","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"Z Chaochen","year":"1994","unstructured":"Chaochen, Z., Jingzhong, Z., Lu, Y., Xiaoshan, L.: Linear duration invariants. In: Langmaack, H., Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 86\u2013109. Springer, Heidelberg (1994). doi:\n10.1007\/3-540-58468-4_161"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:36:55Z","timestamp":1499693815000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}