{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T08:12:41Z","timestamp":1676016761298},"reference-count":69,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2011,11,22]],"date-time":"2011-11-22T00:00:00Z","timestamp":1321920000000},"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,10]]},"DOI":"10.1007\/s10009-011-0217-7","type":"journal-article","created":{"date-parts":[[2011,11,21]],"date-time":"2011-11-21T14:47:18Z","timestamp":1321886838000},"page":"455-474","source":"Crossref","is-referenced-by-count":12,"title":["Functional synthesis for linear arithmetic and sets"],"prefix":"10.1007","volume":"15","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mika\u00ebl","family":"Mayer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philippe","family":"Suter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,11,22]]},"reference":[{"key":"217_CR1","unstructured":"Anand, S., Godefroid, P., Tillmann, N.: Demand-driven compositional symbolic execution. In: Tools and Algorithms for the Construction and Analysis of Systems (2008)"},{"key":"217_CR2","doi-asserted-by":"crossref","unstructured":"Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Hybrid Systems II, pp. 1\u201320 (1995)","DOI":"10.1007\/3-540-60472-3_1"},{"key":"217_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-6894-6","volume-title":"Dependence Analysis for Supercomputing","author":"U.K. Banerjee","year":"1988","unstructured":"Banerjee U.K.: Dependence Analysis for Supercomputing. Kluwer, Norwell (1988)"},{"issue":"3","key":"217_CR4","doi-asserted-by":"crossref","first-page":"614","DOI":"10.1145\/1071596.1071601","volume":"6","author":"B. Boigelot","year":"2005","unstructured":"Boigelot B., Jodogne S., Wolper P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Log. 6(3), 614\u2013633 (2005)","journal-title":"ACM Trans. Comput. Log."},{"key":"217_CR5","volume-title":"The Calculus of Computation","author":"A.R. Bradley","year":"2007","unstructured":"Bradley A.R., Manna Z.: The Calculus of Computation. Springer, Berlin (2007)"},{"issue":"8","key":"217_CR6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"8","key":"217_CR7","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.entcs.2006.11.037","volume":"174","author":"C. Barrett","year":"2007","unstructured":"Barrett C., Shikanian I., Tinelli C.: An abstract decision procedure for satisfiability in the theory of recursive data types. Electron. Notes Theor. Comput. Sci. 174(8), 23\u201337 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"217_CR8","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"2001","unstructured":"Cormen T.H., Leiserson C.E., Rivest R.L., Stein C.: Introduction to Algorithms, 2nd edn. MIT Press and McGraw-Hill, Cambridge (2001)","edition":"2"},{"key":"217_CR9","first-page":"91","volume-title":"Machine Intelligence, vol. 7","author":"D.C. Cooper","year":"1972","unstructured":"Cooper D.C.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds) Machine Intelligence, vol. 7, pp. 91\u2013100. Edinburgh University Press, Edinburgh (1972)"},{"key":"217_CR10","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"217_CR11","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1145\/357062.357064","volume":"1","author":"R.B.K. Dewar","year":"1979","unstructured":"Dewar R.B.K., Grand A., Liu S.-C., Schwartz J.T., Schonberg E.: Programming by refinement, as exemplified by the SETL representation sublanguage. ACM Trans. Program. Lang. Syst. (TOPLAS) 1(1), 27\u201349 (1979). doi: 10.1145\/357062.357064","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"217_CR12","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra E.W.: A Discipline of Programming. Prentice-Hall, Inc., Englewood Cliffs (1976)"},{"key":"217_CR13","doi-asserted-by":"crossref","unstructured":"Emir, B., Odersky, M., Williams, J.: Matching objects with patterns. In: ECOOP (2007)","DOI":"10.1007\/978-3-540-73589-2_14"},{"issue":"4","key":"217_CR14","doi-asserted-by":"crossref","first-page":"839","DOI":"10.1287\/moor.1080.0320","volume":"33","author":"F. Eisenbrand","year":"2008","unstructured":"Eisenbrand F., Shmonin G.: Parametric integer programming in fixed dimension. Math. Oper. Res. 33(4), 839\u2013850 (2008)","journal-title":"Math. Oper. Res."},{"key":"217_CR15","doi-asserted-by":"crossref","unstructured":"Ford, D., Havas, G.: A new algorithm and refined bounds for extended gcd computation. In: ANTS, pp. 145\u2013150 (1996)","DOI":"10.1007\/3-540-61581-4_50"},{"key":"217_CR16","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lilibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI (2002)","DOI":"10.1145\/512529.512558"},{"key":"217_CR17","doi-asserted-by":"crossref","unstructured":"Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718. Springer, Berlin (1979)","DOI":"10.1007\/BFb0062837"},{"key":"217_CR18","doi-asserted-by":"crossref","first-page":"57","DOI":"10.4064\/fm-47-1-57-103","volume":"47","author":"S. Feferman","year":"1959","unstructured":"Feferman S., Vaught R.L.: The first order properties of products of algebraic systems. Fundam. Math. 47, 57\u2013103 (1959)","journal-title":"Fundam. Math."},{"key":"217_CR19","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Cesare, T.: DPLL(T): fast decision procedures. In: CAV, pp. 175\u2013188 (2004)","DOI":"10.1007\/978-3-540-27813-9_14"},{"issue":"2","key":"217_CR20","first-page":"333","volume":"113","author":"S. Ginsburg","year":"1964","unstructured":"Ginsburg S., Spanier E.: Bounded algol-like languages. Trans. Am. Math. Soc. 113(2), 333\u2013368 (1964)","journal-title":"Trans. Am. Math. Soc."},{"issue":"2","key":"217_CR21","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1966.16.285","volume":"16","author":"S. Ginsburg","year":"1966","unstructured":"Ginsburg S., Spanier E.: Semigroups, Presburger formulas and languages. Pac. J. Math. 16(2), 285\u2013296 (1966)","journal-title":"Pac. J. Math."},{"key":"217_CR22","unstructured":"Hamza, J., Jobstmann, B., Kuncak, V.: Synthesis for regular specifications over unbounded domains. In: FMCAD, pp. 101\u2013109 (2010)"},{"key":"217_CR23","volume-title":"Model Theory. Encyclopedia of Mathematics and its Applications, vol. 42","author":"W. Hodges","year":"1993","unstructured":"Hodges W.: Model Theory. Encyclopedia of Mathematics and its Applications, vol. 42. Cambridge University Press, London (1993)"},{"key":"217_CR24","unstructured":"Jacobs, S.: Hierarchic decision procedures for verification. PhD thesis, Universit\u00e4t des Saarlandes (2010)"},{"key":"217_CR25","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"217_CR26","unstructured":"Jones, S.P. et\u00a0al.: Haskell 98 language and libraries: the revised report (2010)"},{"key":"217_CR27","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial evaluation and automatic program generation (available on the Web) (1993)"},{"key":"217_CR28","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: a tool for property synthesis. In: CAV. LNCS, vol. 4590 (2007)"},{"key":"217_CR29","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19\/20","author":"J. Jaffar","year":"1994","unstructured":"Jaffar J., Maher M.J.: Constraint logic programming: a survey. J. Log. Program. 19\/20, 503\u2013581 (1994)","journal-title":"J. Log. Program."},{"key":"217_CR30","doi-asserted-by":"crossref","unstructured":"K\u00f6ksal, A.S., Kuncak, V., Suter, P.: Scala to the power of Z3: integrating SMT and programming. In: CADE, pp. 400\u2013406 (2011)","DOI":"10.1007\/978-3-642-22438-6_30"},{"key":"217_CR31","doi-asserted-by":"crossref","unstructured":"Klaedtke, F.: On the automata size for Presburger arithmetic. Technical Report 186, Institute of Computer Science at Freiburg University (2003)","DOI":"10.1109\/LICS.2004.1319605"},{"key":"217_CR32","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA version 1.4 user manual. BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus (2001)"},{"issue":"3","key":"217_CR33","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.: Deciding Boolean algebra with Presburger arithmetic. J. Autom. Reason. 36(3), 213\u2013236 (2006)","journal-title":"J. Autom. Reason."},{"key":"217_CR34","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Piskac, R., Suter, P.: Ordered sets in the calculus of data structures. In: CSL, pp. 34\u201348 (2010)","DOI":"10.1007\/978-3-642-15205-4_5"},{"key":"217_CR35","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Piskac, R., Suter, P., Wies, T.: Building a calculus of data structures. In:VMCAI. LNCS, vol. 5944 (2010)","DOI":"10.1007\/978-3-642-11319-2_6"},{"key":"217_CR36","unstructured":"Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In: CADE-21. LNCS, vol. 4603 (2007)"},{"key":"217_CR37","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Schwartzbach, M.I.: Graph types. In: POPL, Charleston, SC (1993)","DOI":"10.1145\/158511.158628"},{"key":"217_CR38","doi-asserted-by":"crossref","unstructured":"Kukula, J.H., Shiple, T.R.: Building circuits from relations. In: CAV (2000)","DOI":"10.1007\/10722167_12"},{"key":"217_CR39","doi-asserted-by":"crossref","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: CAV, pp. 476\u2013490 (2005)","DOI":"10.1007\/11513988_47"},{"key":"217_CR40","doi-asserted-by":"crossref","unstructured":"Monniaux, D.P.: Automatic modular abstractions for linear constraints. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 140\u2013151 (2009)","DOI":"10.1145\/1480881.1480899"},{"key":"217_CR41","unstructured":"Moskal, M.: Satisfiability modulo software. PhD thesis, University of Wroc\u0142aw (2009)"},{"issue":"3","key":"217_CR42","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/362566.362568","volume":"14","author":"Z. Manna","year":"1971","unstructured":"Manna Z., Waldinger R.J.: Toward automatic program synthesis. Commun. ACM 14(3), 151\u2013165 (1971)","journal-title":"Commun. ACM"},{"issue":"1","key":"217_CR43","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna Z., Waldinger R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90\u2013121 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"217_CR44","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Linear quantifier elimination. In: IJCAR (2008)","DOI":"10.1007\/978-3-540-71070-7_3"},{"key":"217_CR45","doi-asserted-by":"crossref","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. In: POPL, pp. 151\u2013157 (1978)","DOI":"10.1145\/512760.512776"},{"key":"217_CR46","volume-title":"Programming in Scala: A Comprehensive Step-by-Step Guide","author":"M. Odersky","year":"2008","unstructured":"Odersky M., Spoon L., Venners B.: Programming in Scala: A Comprehensive Step-by-Step Guide. Artima Press, Walnut Creek (2008)"},{"key":"217_CR47","unstructured":"Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: VMCAI. LNCS, vol. 4905 (2008)"},{"key":"217_CR48","unstructured":"Piskac, R., Kuncak, V.: Linear arithmetic with stars. In: CAV. LNCS, vol. 5123 (2008)"},{"key":"217_CR49","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: VMCAI (2006)","DOI":"10.1007\/11609773_24"},{"key":"217_CR50","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL (1989)","DOI":"10.1145\/75277.75293"},{"issue":"8","key":"217_CR51","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"Pugh W.: A practical algorithm for exact array dependence analysis. Commun. ACM 35(8), 102\u2013114 (1992)","journal-title":"Commun. ACM"},{"key":"217_CR52","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1998","unstructured":"Schrijver A.: Theory of Linear and Integer Programming. Wiley, New York (1998)"},{"key":"217_CR53","doi-asserted-by":"crossref","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: POPL (2010)","DOI":"10.1145\/1706299.1706325"},{"key":"217_CR54","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4302-0285-1","volume-title":"Expert F#","author":"D. Syme","year":"2007","unstructured":"Syme D., Granicz A., Cisternino A.: Expert F#. Apress, New York (2007)"},{"key":"217_CR55","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL (2010)","DOI":"10.1145\/1706299.1706337"},{"issue":"2","key":"217_CR56","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1145\/357162.357166","volume":"4","author":"M. Sharir","year":"1982","unstructured":"Sharir M.: Some observations concerning formal differentiation of set theoretic expressions. Trans. Program. Lang. Syst. 4(2), 196\u2013226 (1982)","journal-title":"Trans. Program. Lang. Syst."},{"key":"217_CR57","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Arnold, G., Tancau, L., Bod\u00edk, R., Saraswat, V.A., Seshia, S.A.: Sketching stencils. In: PLDI (2007)","DOI":"10.1145\/1250734.1250754"},{"key":"217_CR58","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bod\u00edk, R.: Sketching concurrent data structures. In: PLDI (2008)","DOI":"10.1145\/1375581.1375599"},{"key":"217_CR59","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"217_CR60","doi-asserted-by":"crossref","first-page":"1207","DOI":"10.1137\/S0097539793246252","volume":"24","author":"R.C. Sekar","year":"1995","unstructured":"Sekar R.C., Ramesh R., Ramakrishnan I.V.: Adaptive pattern matching. SIAM J. Comput. 24, 1207\u20131234 (1995)","journal-title":"SIAM J. Comput."},{"key":"217_CR61","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E., Bacon, D.F., Rinetzky, N.: Cgcexplorer: a semi-automated search procedure for provably correct concurrent collectors. In: PLDI, pp. 456\u2013467 (2007)","DOI":"10.1145\/1273442.1250787"},{"key":"217_CR62","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: TACAS (2009)","DOI":"10.1007\/978-3-642-00768-2_13"},{"key":"217_CR63","doi-asserted-by":"crossref","unstructured":"Weispfenning, V.: Complexity and uniformity of elimination in Presburger arithmetic. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation, pp. 48\u201353 (1997)","DOI":"10.1145\/258726.258746"},{"key":"217_CR64","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.: Efficiently solving quantified bit-vector formulas. In: FMCAD, pp. 239\u2013246 (2010)"},{"key":"217_CR65","doi-asserted-by":"crossref","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: FroCoS: Frontiers in Combining Systems (2009)","DOI":"10.1007\/978-3-642-04222-5_23"},{"key":"217_CR66","doi-asserted-by":"crossref","unstructured":"Yessenov, K., Piskac, R., Kuncak, V.: Collections, cardinalities, and relations. In: VMCAI. LNCS, vol. 5944 (2010)","DOI":"10.1007\/978-3-642-11319-2_27"},{"key":"217_CR67","unstructured":"Zarba, C.G.: A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator. In: 18th International Workshop on Unification (2004)"},{"issue":"1","key":"217_CR68","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-005-3075-8","volume":"34","author":"C.G. Zarba","year":"2005","unstructured":"Zarba C.G.: Combining sets with cardinals. J. Autom. Reason. 34(1), 1\u201329 (2005)","journal-title":"J. Autom. Reason."},{"key":"217_CR69","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: PLDI (2008)","DOI":"10.1145\/1375581.1375624"}],"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-011-0217-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0217-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0217-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T22:14:04Z","timestamp":1560982444000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0217-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11,22]]},"references-count":69,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["217"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0217-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11,22]]}}}