{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:22:11Z","timestamp":1737436931621,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_40","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"352-365","source":"Crossref","is-referenced-by-count":14,"title":["Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra"],"prefix":"10.1007","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[]},{"given":"Zijiang","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[]},{"given":"Franjo","family":"Ivan\u010di\u0107","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"40_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-44898-5_19","volume-title":"Static Analysis","author":"R. Bagnara","year":"2003","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra (LNCS 2694). In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 337\u2013354. Springer, Heidelberg (2003)"},{"key":"40_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-540-24622-0_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Bagnara","year":"2004","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 135\u2013148. Springer, Heidelberg (2004)"},{"key":"40_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Programming Language Design and Implementation (2001)","DOI":"10.1145\/378795.378846"},{"issue":"8","key":"40_CR4","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. on Computer\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. on Computer"},{"key":"40_CR5","doi-asserted-by":"crossref","unstructured":"Bultan, T., Gerber, R., League, C.: Verifying systems with integer constraints and boolean predicates: A composite approach. In: Symposium on Software Testing and Analysis, pp. 113\u2013123 (1998)","DOI":"10.1145\/271771.271799"},{"key":"40_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","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, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"40_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"40_CR8","doi-asserted-by":"crossref","unstructured":"Coen-Porisini, A., Denaro, G., Ghezzi, C., Pezze, M.: Using symbolic execution for verifying safety-critical systems. In: European Software Engineering Conference\/Foundations of Software Engineering, pp. 142\u2013151 (2001)","DOI":"10.1145\/503209.503230"},{"key":"40_CR9","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: International Symposium on Programming, pp. 106\u2013126 (1976)"},{"key":"40_CR10","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.\u00a0631, pp. 269\u2013295. Springer, Heidelberg (1992)"},{"key":"40_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Programming Languages, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"40_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11817963_41","volume-title":"Computer Aided Verification","author":"D. Gopan","year":"2006","unstructured":"Gopan, D., Reps, T.W.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 452\u2013466. Springer, Heidelberg (2006)"},{"key":"40_CR13","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., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"40_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11691372_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2006","unstructured":"Gulavani, B.S., Rajamani, S.K.: Counterexample driven refinement for abstract interpretation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 474\u2013488. Springer, Heidelberg (2006)"},{"key":"40_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-56922-7_28","volume-title":"Computer Aided Verification","author":"N. Halbwachs","year":"1993","unstructured":"Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 333\u2013346. Springer, Heidelberg (1993)"},{"issue":"2","key":"40_CR16","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in Systems Design\u00a011(2), 157\u2013185 (1997)","journal-title":"Formal Methods in Systems Design"},{"key":"40_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-60472-3_13","volume-title":"Hybrid Systems II","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H.: A note on abstract interpretation strategies for hybrid automata. In: Hybrid Systems II. LNCS, vol.\u00a0999, pp. 252\u2013264. Springer, Heidelberg (1995)"},{"key":"40_CR18","doi-asserted-by":"crossref","unstructured":"Ivan\u010di\u0107, F., Shlyakhter, I., Gupta, A., Ganai, M.K., Kahlon, V., Wang, C., Yang, Z.: Model checking C program using F-Soft. In: IEEE International Conference on Computer Design, pp. 297\u2013308 (2005)","DOI":"10.1109\/ICCD.2005.77"},{"key":"40_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F. Ivan\u010di\u0107","year":"2005","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Shlyakhter, I., Ganai, M.K., Gupta, A., Ashar, P.: F-Soft: Software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"40_CR20","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.\u00a01694, pp. 39\u201350. Springer, Heidelberg (1999)"},{"key":"40_CR21","volume-title":"Computer-Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ (1994)"},{"key":"40_CR22","unstructured":"The Parma\u00a0Polyhedra Library. University of Parma, Italy, http:\/\/www.cs.unipr.it\/ppl\/"},{"key":"40_CR23","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1994","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA (1994)"},{"key":"40_CR24","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"40_CR25","unstructured":"The\u00a0Omega Project. University of Maryland, http:\/\/www.cs.umd.edu\/projects\/omega\/"},{"issue":"2","key":"40_CR26","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1109\/71.342135","volume":"6","author":"W. Pugh","year":"1994","unstructured":"Pugh, W., Wonnacott, D.: Going beyond integer programming with the Omega test to eliminate false data dependences. IEEE Trans. on Parallel and Distributed Systems\u00a06(2), 204\u2013211 (1994)","journal-title":"IEEE Trans. on Parallel and Distributed Systems"},{"key":"40_CR27","doi-asserted-by":"crossref","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Symposium on Programming (1981)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"40_CR28","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Ivan\u010di\u0107, F., Shlyakhter, I., Gupta, A.: Static analysis in disjunctive numerical domains. In: Symposium on Static Analysis (2006)","DOI":"10.1007\/11823230_2"},{"key":"40_CR29","doi-asserted-by":"crossref","unstructured":"Shiple, T.R., Hojati, R., Sangiovanni-Vincentelli, A.L., Brayton, R.K.: Heuristic minimization of BDDs using don\u2019t cares. In: Design Automation Conference, pp. 225\u2013231 (1994)","DOI":"10.1145\/196244.196360"},{"key":"40_CR30","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package. University of Colorado at Boulder, ftp:\/\/vlsi.colorado.edu\/pub\/"},{"key":"40_CR31","unstructured":"Wang, C., Yang, Z., Ivan\u010di\u0107, F., Gupta, A.: Disjunctive image computation for embedded software verification. In: Design, Automation and Test in Europe, pp. 1205\u20131210 (2006)"},{"key":"40_CR32","unstructured":"Yang, Z., Wang, C., Ivan\u010di\u0107, F., Gupta, A.: Mixed symbolic representations for model checking software programs. In: Formal Methods and Models for Codesign, pp. 17\u201324 (2006)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T19:01:12Z","timestamp":1737399672000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_40","relation":{},"subject":[]}}