{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,16]],"date-time":"2025-02-16T14:10:12Z","timestamp":1739715012845,"version":"3.37.1"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642113185"},{"type":"electronic","value":"9783642113192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11319-2_15","type":"book-chapter","created":{"date-parts":[[2010,1,6]],"date-time":"2010-01-06T05:00:05Z","timestamp":1262754005000},"page":"180-196","source":"Crossref","is-referenced-by-count":14,"title":["Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction"],"prefix":"10.1007","author":[{"given":"Yungbum","family":"Jung","sequence":"first","affiliation":[]},{"given":"Soonho","family":"Kong","sequence":"additional","affiliation":[]},{"given":"Bow-Yaw","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Kwangkeun","family":"Yi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1145\/1040305.1040314","volume-title":"POPL","author":"R. Alur","year":"2005","unstructured":"Alur, R., Cern\u00fd, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for java classes. In: POPL, pp. 98\u2013109. ACM, New York (2005)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"548","DOI":"10.1007\/11513988_52","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2005","unstructured":"Alur, R., Madhusudan, P., Nam, W.: Symbolic compositional verification by learning assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 548\u2013562. Springer, Heidelberg (2005)"},{"issue":"2","key":"15_CR3","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D. Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation\u00a075(2), 87\u2013106 (1987)","journal-title":"Information and Computation"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/978-3-540-30579-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.: Shape analysis by predicate abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 164\u2013180. Springer, Heidelberg (2005)"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1007\/978-3-540-24730-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Das, S., Rajamani, S.K.: Refining approximations in software predicate abstraction. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 388\u2013403. Springer, Heidelberg (2004)"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1006\/inco.1995.1164","volume":"123","author":"N.H. Bshouty","year":"1995","unstructured":"Bshouty, N.H.: Exact learning boolean functions via the monotone theory. Information and Computation\u00a0123, 146\u2013153 (1995)","journal-title":"Information and Computation"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-3-642-00768-2_3","volume-title":"TACAS 2009","author":"Y.F. Chen","year":"2009","unstructured":"Chen, Y.F., Farzan, A., Clarke, E.M., Tsay, Y.K., Wang, B.Y.: Learning minimal separating DFA\u2019s for compositional verification. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 31\u201345. Springer, Heidelberg (2009)"},{"key":"15_CR8","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.M. Clarke","year":"2000","unstructured":"Clarke, E.M., 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":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"15_CR10","first-page":"84","volume-title":"POPL","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201396. ACM, New York (1978)"},{"unstructured":"Dutertre, B., Moura, L.D.: The Yices SMT solver. Technical report, SRI International (2006)","key":"15_CR11"},{"key":"15_CR12","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/503272.503291","volume-title":"POPL","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191\u2013202. ACM, New York (2002)"},{"key":"15_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":"15_CR14","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1145\/1542476.1542518","volume-title":"PLDI","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: PLDI, pp. 375\u2013385. ACM, New York (2009)"},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1145\/1328438.1328468","volume-title":"POPL","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235\u2013246. ACM, New York (2008)"},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/1375581.1375616","volume-title":"PLDI","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281\u2013292. ACM, New York (2008)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-540-93900-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 120\u2013135. Springer, Heidelberg (2009)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-73368-3_45","volume-title":"Computer Aided Verification","author":"A. Gupta","year":"2007","unstructured":"Gupta, A., McMillan, K.L., Fu, Z.: Automated assumption generation for compositional verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 420\u2013432. Springer, Heidelberg (2007)"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"634","DOI":"10.1007\/978-3-642-02658-4_48","volume-title":"CAV 2009","author":"A. Gupta","year":"2009","unstructured":"Gupta, A., Rybalchenko, A.: Invgen: An efficient invariant generator. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 634\u2013640. Springer, Heidelberg (2009)"},{"unstructured":"Jung, Y., Kong, S., Bow-Yaw, W., Yi, K.: Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction. Technical Memorandum ROSAEC-2009-004, Research On Software Analysis for Error-Free Computing (2009)","key":"15_CR20"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"FASE 2009","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: FASE 2009. LNCS, pp. 470\u2013485. Springer, Heidelberg (2009)"},{"key":"15_CR22","series-title":"EATCS","volume-title":"Decision Procedures an algorithmic point of view","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures an algorithmic point of view. EATCS. Springer, Heidelberg (2008)"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/978-3-540-24622-0_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.E., Bryant, A.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 267\u2013281. Springer, Heidelberg (2004)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Bryant, A.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 141\u2013153. Springer, Heidelberg (2003)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 413\u2013427. Springer, Heidelberg (2008)"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11547662_19","volume-title":"Static Analysis","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Wies, T.: Boolean heaps. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 268\u2013283. Springer, Heidelberg (2005)"},{"key":"15_CR27","volume-title":"Discrete Mathematics and Its Applications","author":"K.H. Rosen","year":"2006","unstructured":"Rosen, K.H.: Discrete Mathematics and Its Applications. McGraw-Hill Higher Education, New York (2006)"},{"key":"15_CR28","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1145\/1542476.1542501","volume-title":"PLDI","author":"S. Srivastava","year":"2009","unstructured":"Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: PLDI, pp. 223\u2013234. ACM, New York (2009)"},{"key":"15_CR29","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1145\/1375581.1375624","volume-title":"PLDI","author":"K. Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: PLDI, pp. 349\u2013361. ACM, New York (2008)"},{"key":"15_CR30","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1145\/1542476.1542514","volume-title":"PLDI","author":"K. Zee","year":"2009","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: An integrated proof language for imperative programs. In: PLDI, pp. 338\u2013351. ACM, New York (2009)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11319-2_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,16]],"date-time":"2025-02-16T13:43:18Z","timestamp":1739713398000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11319-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642113185","9783642113192"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11319-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}