{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:30:50Z","timestamp":1725474650351},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540499947"},{"type":"electronic","value":"9783540499954"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11944836_37","type":"book-chapter","created":{"date-parts":[[2006,11,27]],"date-time":"2006-11-27T23:48:02Z","timestamp":1164671282000},"page":"405-416","source":"Crossref","is-referenced-by-count":1,"title":["Validity Checking for Finite Automata over Linear Arithmetic Constraints"],"prefix":"10.1007","author":[{"given":"Gary","family":"Wassermann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"37_CR1","unstructured":"Borland, M.: Advanced SQL Command Injection: Applying defense-in-depth practices in web-enabled database applications (2002)"},{"key":"37_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","volume-title":"Static Analysis","author":"A.S. Christensen","year":"2003","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 1\u201318. Springer, Heidelberg (2003), URL: http:\/\/www.brics.dk\/JSA\/"},{"key":"37_CR3","first-page":"83","volume":"21","author":"Y. Matiyasevich","year":"1970","unstructured":"Matiyasevich, Y.: Solution of the tenth problem of Hilbert. Mat. Lapok\u00a021, 83\u201387 (1970)","journal-title":"Mat. Lapok"},{"key":"37_CR4","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951)","DOI":"10.1525\/9780520348097"},{"key":"37_CR5","doi-asserted-by":"crossref","unstructured":"Gould, C., Su, Z., Devanbu, P.: Static checking of dynamically generated queries in database applications. In: Proc. ICSE 2004 (2004)","DOI":"10.1109\/ICSE.2004.1317486"},{"key":"37_CR6","doi-asserted-by":"crossref","unstructured":"Wassermann, G., Su, Z.: Validity Checking for Finite Automata over Linear Arithmetic. Technical report, University of California, Davis, Computer Science Dept. (2006)","DOI":"10.1007\/11944836_37"},{"key":"37_CR7","doi-asserted-by":"crossref","unstructured":"Danzer, L., Gr\u00fcnbaum, B., Klee, V.: Helly\u2019s theorem and its relatives. In: Proceedings of the Symposium on Pure Mathematics. Convexity, vol.\u00a07, pp. 101\u2013180. AMS (1963)","DOI":"10.1090\/pspum\/007\/0157289"},{"key":"37_CR8","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. A Theory and Formal Languages (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"37_CR9","first-page":"21","volume-title":"SAS","author":"P. Wolper","year":"1995","unstructured":"Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints (extended abstract). In: SAS, pp. 21\u201332. Springer, Heidelberg (1995)"},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: Proc. Supercomputing, pp. 4\u201313 (1991)","DOI":"10.1145\/125826.125848"},{"key":"37_CR11","unstructured":"Bledsoe, W.: The Sup-Inf method in Presburger arithmetic. Technical report, University of Texas Math. Department (1974)"},{"key":"37_CR12","unstructured":"Nelson, G.: Techniques for program verification. Technical report, Xerox PARC (1981)"},{"key":"37_CR13","unstructured":"Pratt, V.: Two easy theories whose combination is hard. Technical report, MIT (1977)"},{"key":"37_CR14","doi-asserted-by":"crossref","unstructured":"Shostak, R.: Deciding linear inequalities by computing loop residues. J. ACM 28 (1981)","DOI":"10.1145\/322276.322288"},{"key":"37_CR15","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1137\/0209063","volume":"9","author":"B. Aspvall","year":"1980","unstructured":"Aspvall, B., Shiloach, Y.: A polynomial time algorithm for solving systems of linear inequalities with two variables per inequality. SIAM Computing\u00a09, 827\u2013845 (1980)","journal-title":"SIAM Computing"},{"key":"37_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-24730-2_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z. Su","year":"2004","unstructured":"Su, Z., Wagner, D.: A class of polynomially solvable range constraints for interval analysis without widenings and narrowings. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 280\u2013295. Springer, Heidelberg (2004)"},{"key":"37_CR17","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Symposium on Programming, pp. 106\u2013130 (1976)","DOI":"10.1145\/800022.808314"},{"key":"37_CR18","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: POPL, pp. 234\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"37_CR19","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. TOPLAS\u00a01, 245\u2013257 (1979)","journal-title":"TOPLAS"},{"key":"37_CR20","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: Proc. PLDI (1998)","DOI":"10.1145\/277650.277752"},{"key":"37_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. J. ACM\u00a031, 1\u201312 (1984)","journal-title":"J. ACM"},{"key":"37_CR22","doi-asserted-by":"crossref","unstructured":"Owre, S., Shankar, N., Rushby, J.: PVS: A Prototype Verification System. In: Proc. CADE 11 (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"37_CR23","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Browne, A., Chang, E., Col\u00f3n, M., Kapur, A., Manna, Z., Sipma, H., Uribe, T.E.: STeP: Deductive-algorithmic verification of reactive and real-time systems. In: Proc. CAV (1996)","DOI":"10.1007\/3-540-61474-5_92"},{"key":"37_CR24","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Dill, D.L., Levitt, J.R.: Validity Checking for Combinations of Theories with Equality. In: Proc. FMCAD, pp. 187\u2013201 (1996)","DOI":"10.1007\/BFb0031808"},{"key":"37_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2004","unstructured":"Barrett, C.W., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"37_CR26","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1142\/S0218195995000222","volume":"5","author":"D. Avis","year":"1995","unstructured":"Avis, D., Houle, M.E.: Computational aspects of Helly\u2019s theorem and its relatives. International Journal of Computational Geometry Applications\u00a05, 357\u2013367 (1995)","journal-title":"International Journal of Computational Geometry Applications"},{"key":"37_CR27","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/BF02574379","volume":"12","author":"N. Amenta","year":"1994","unstructured":"Amenta, N.: Helly-type theorems and generalized linear programming. Discrete & Computational Geometry\u00a012, 241\u2013261 (1994)","journal-title":"Discrete & Computational Geometry"}],"container-title":["Lecture Notes in Computer Science","FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11944836_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,5]],"date-time":"2021-08-05T01:23:29Z","timestamp":1628126609000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11944836_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540499947","9783540499954"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/11944836_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}