{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:24:11Z","timestamp":1725891851105},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540472377"},{"type":"electronic","value":"9783540472384"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_27","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T05:21:43Z","timestamp":1160457703000},"page":"352-368","source":"Crossref","is-referenced-by-count":3,"title":["Predicate Abstraction of Programs with Non-linear Computation"],"prefix":"10.1007","author":[{"given":"Songtao","family":"Xia","sequence":"first","affiliation":[]},{"given":"Ben","family":"Di Vito","sequence":"additional","affiliation":[]},{"given":"Cesar","family":"Munoz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","volume-title":"Interval Methods for System of Equations","author":"A. Neumaier","year":"1990","unstructured":"Neumaier, A.: Interval Methods for System of Equations. Cambridge University Press, Cambridge (1990)"},{"key":"27_CR2","volume-title":"Introduction to Interval Computations","author":"G. Alefeld","year":"1983","unstructured":"Alefeld, G., Herzberger, J.: Introduction to Interval Computations. Academic Press, London (1983)"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"Computer Aided Verification","author":"E. Asarin","year":"2002","unstructured":"Asarin, E., Dang, T., Maler, O.: The d\/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 365\u2013370. Springer, Heidelberg (2002)"},{"key":"27_CR4","unstructured":"Ball, T.: Formalizing counter-example driven predicate refinement with weakest preconditions. Technical Report MSR-TR-2004-134, Microsoft Research (2004)"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-540-27813-9_36","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 457\u2013461. Springer, Heidelberg (2004)"},{"key":"27_CR6","first-page":"268","volume-title":"Proceedings of Programming Languages Design and Implementation (PLDI) 2001","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic Predicate Abstraction of C Programs. In: Proceedings of Programming Languages Design and Implementation (PLDI) 2001, pp. 268\u2013283. ACM Press, New York (2001)"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"C. Barret","year":"2005","unstructured":"Barret, C., Tinelli, C.: Theory and practice of decision procedures for combinations of theories. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, Springer, Heidelberg (2005)"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, Springer, Heidelberg (2004)"},{"key":"27_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing Abstractions of Infinite State Systems Compositionally and Automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-27864-1_2","volume-title":"Static Analysis","author":"D. Beyer","year":"2004","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: The BLAST query language for software verification. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 2\u201318. Springer, Heidelberg (2004)"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G. Collins","year":"1975","unstructured":"Collins, G.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTREE analyser. In: Proceedings of The European Symposium on Programming, pp. 21\u201330 (2005)","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D., Park, S.J.: Experience with Predicate Abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Proceedings of Conference on Formal Methods in Computer-Aided Design, Portland, Oregon (November 2002)","DOI":"10.1007\/3-540-36126-X_2"},{"key":"27_CR17","unstructured":"Detlefs, D., Nelson, G., Saxe, J.: Simplify: A theorem prover for program checking (2003)"},{"key":"27_CR18","unstructured":"Dowek, G., Geser, A., Mu\u00f1oz, C.: Tactical conflict detection and resolution in a 3-D airspace. In: Proceedings of the 4th USA\/Europe Air Traffic Management R&DSeminar, ATM 2001, Santa Fe, New Mexico, 2001. A long version appears as report NASA\/CR-2001-210853 ICASE Report No 2001-7"},{"key":"27_CR19","unstructured":"Dwyer, M., Hatcliff, J., Joehanes, R., Laubach, S., Pasareanu, C., Visser, R., Zheng, H.: Tool-supported Program Abstraction for Finite-state Verification"},{"key":"27_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.-C., Owre, S., Rue\u00df, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 246\u2013249. Springer, Heidelberg (2001)"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"6","key":"27_CR22","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1023\/A:1014750702474","volume":"7","author":"L. Granvilliers","year":"2001","unstructured":"Granvilliers, L.: On the combination of interval constraint solvers. Reliable Computing\u00a07(6), 467\u2013483 (2001)","journal-title":"Reliable Computing"},{"key":"27_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-49481-2_18","volume-title":"Principles and Practice of Constraint Programming - CP98","author":"W. Harvey","year":"1998","unstructured":"Harvey, W., Stuckey, P.J.: Constraint representation for propagation. In: Maher, M.J., Puget, J.-F. (eds.) CP 1998. LNCS, vol.\u00a01520, pp. 235\u2013245. Springer, Heidelberg (1998)"},{"key":"27_CR24","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5073.001.0001","volume-title":"Numerica, A Modeling Language for Global Optimization","author":"P.V. Hentenryck","year":"1997","unstructured":"Hentenryck, P.V., Michel, L., Deville, Y.: Numerica, A Modeling Language for Global Optimization. MIT Press, Cambridge (1997)"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstraction from Proofs. In: Proceedings of ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages (POPL), pp. 232\u2013244 (2004)","DOI":"10.1145\/964001.964021"},{"key":"27_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T. Henzinger","year":"2002","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Necula, G., Sutre, G., Weimer, W.: Temporal-Safety Proofs for Systems Code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"key":"27_CR27","doi-asserted-by":"crossref","unstructured":"Yamamura, K., Kawata, H., Tokue, A.: Interval analysis using linear programming. In: Proceedings of BIT 38, pp. 188\u2013201 (1998)","DOI":"10.1007\/BF02510924"},{"key":"27_CR28","doi-asserted-by":"crossref","unstructured":"Granvilliers, L., Benhamou, F.: Realpaver: An interval solver using constraint satisfaction techniques. ACM Transactions on Mathematical Software (accepted for publication)","DOI":"10.1145\/1132973.1132980"},{"key":"27_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/3-540-44898-5_18","volume-title":"Static Analysis","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Craig interpolation and reachability analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, p. 336. Springer, Heidelberg (2003)"},{"key":"27_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Compiler Construction","author":"S. McPeak","year":"2002","unstructured":"McPeak, S., Necula, G.C., Rahul, S.P., Weimer, W.: CIL: Intermediate Languages and Tools for C Program Analysis and Transformation. In: Horspool, R.N. (ed.) CC 2002 and ETAPS 2002. LNCS, vol.\u00a02304, Springer, Heidelberg (2002)"},{"key":"27_CR31","volume-title":"Interval Analysis","author":"R. Moore","year":"1966","unstructured":"Moore, R.: Interval Analysis. Prentice-Hall, Englewood Cliffs (1966)"},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J., Shankar, N.: Pvs: A prototype verification system (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"27_CR33","unstructured":"Ratschan, S.: Slides, available at http:\/\/www.mpi-sb.mpg.de\/~ratschan\/decproc1.pdf"},{"key":"27_CR34","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of Artificial Intelligence and Symbolic Computation","author":"S. Ratschan","year":"2002","unstructured":"Ratschan, S.: Continuous first-order constraint satisfaction. In: Proceedings of Artificial Intelligence and Symbolic Computation. LNCS, Springer, Heidelberg (2002)"},{"key":"27_CR35","volume-title":"Principles of Mathematical Analysis","author":"W. Rudin","year":"1976","unstructured":"Rudin, W.: Principles of Mathematical Analysis, 3rd edn., ch.\u00a010. McGraw-Hill, New York (1976)","edition":"3"},{"key":"27_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H. Saidi","year":"1999","unstructured":"Saidi, H., Shankar, N.: Abstract and Model-check While You Prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"27_CR37","doi-asserted-by":"crossref","unstructured":"Schmidt, D.: Data Flow Analysis is Model Checking of Abstract Interpretation. In: Proceedings of SIGPLAN Symposium on Principles of Programming Languages (POPL 1998) (1998)","DOI":"10.1145\/268946.268950"},{"key":"27_CR38","unstructured":"Tarski, A.: Logic, Semantics, Metamathematics, papers from 1923 to 1938. Hackett Publishing Company (1983) English Version, original in Polish"},{"key":"27_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/11538363_18","volume-title":"Computer Science Logic","author":"A. Tiwari","year":"2005","unstructured":"Tiwari, A.: An algebraic approach for the unsatisfiability of nonlinear constraints. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 248\u2013262. Springer, Heidelberg (2005)"},{"key":"27_CR40","unstructured":"Visser, W., Park, S., Penix, J.: Applying Predicate Abstraction to Model Check Object-oriented Programs. In: Proceedings of the 33rd ACM SIGSOFT Workshop on Formal Methods in Software Practice,"},{"key":"27_CR41","doi-asserted-by":"crossref","unstructured":"Adams, W., Loustaunau, P.: An Introduction to Gr\u00f6bner Bases. American Mathematical Society (1994)","DOI":"10.1090\/gsm\/003"},{"key":"27_CR42","unstructured":"Wallace, M., Novello, S., Schimpf, J.: ECLiPSe: A platform for constraint logic programming (1997)"},{"key":"27_CR43","doi-asserted-by":"crossref","unstructured":"Xia, S., Vito, B.D., Mu\u00f1oz, C.: Automated test case generations for non-linear engineering programs. In: Proceedings of the Nineenth International Conference on Automated Software Engineering (2005)","DOI":"10.1145\/1101908.1101951"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,21]],"date-time":"2019-04-21T15:23:11Z","timestamp":1555860191000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/11901914_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}