{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T12:16:12Z","timestamp":1725884172657},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319572871"},{"type":"electronic","value":"9783319572888"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57288-8_18","type":"book-chapter","created":{"date-parts":[[2017,4,8]],"date-time":"2017-04-08T02:45:05Z","timestamp":1491619505000},"page":"265-281","source":"Crossref","is-referenced-by-count":5,"title":["Systematic Predicate Abstraction Using Variable Roles"],"prefix":"10.1007","author":[{"given":"Yulia","family":"Demyanova","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,9]]},"reference":[{"key":"18_CR1","volume-title":"Compilers, Principles. Techniques","author":"AV Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers, Principles. Techniques. Addison Wesley, Boston (1986)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-319-03077-7_18","volume-title":"Hardware and Software: Verification and Testing","author":"S Apel","year":"2013","unstructured":"Apel, S., Beyer, D., Friedberger, K., Raimondi, F., Rhein, A.: Domain types: abstract-domain selection based on variable usage. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 262\u2013278. Springer, Cham (2013). doi: 10.1007\/978-3-319-03077-7_18"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"887","DOI":"10.1007\/978-3-662-49674-9_55","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2016","unstructured":"Beyer, D.: Reliable and reproducible competition results with benchexec and witnesses (report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887\u2013904. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_55"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-23404-5_3","volume-title":"Model Checking Software","author":"D Beyer","year":"2015","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Refinement selection. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 20\u201338. Springer, Cham (2015). doi: 10.1007\/978-3-319-23404-5_3"},{"issue":"5","key":"18_CR5","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/978-3-319-21690-4_39","volume-title":"Computer Aided Verification","author":"Y Demyanova","year":"2015","unstructured":"Demyanova, Y., Pani, T., Veith, H., Zuleger, F.: Empirical software metrics for benchmarking of verification tools. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 561\u2013579. Springer, Cham (2015). doi: 10.1007\/978-3-319-21690-4_39"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"Demyanova, Y., Pani, T., Veith, H., Zuleger, F.: Empirical software metrics for benchmarking of verification tools. Int. J. Form. Methods Syst. Des., 1\u201328 (2017). doi: 10.1007\/s10703-016-0264-5 . http:\/\/link.springer.com\/article\/10.1007%2Fs10703-016-0264-5","DOI":"10.1007\/s10703-016-0264-5"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Demyanova, Y., Veith, H., Zuleger, F.: On the concept of variable roles and its use in software analysis. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 226\u2013230. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679414"},{"key":"18_CR10","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1145\/2544173.2509511","volume":"48","author":"I Dillig","year":"2013","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference. ACM SIGPLAN Not. 48, 443\u2013456 (2013). ACM","journal-title":"ACM SIGPLAN Not."},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Engler, D., Chen, D.Y., Hallem, S., Chou, A., Chelf, B.: Bugs as deviant behavior: a general approach to inferring errors in systems code. In: Operating Systems Principles (SOSP), vol. 35. ACM (2001)","DOI":"10.1145\/502034.502041"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: Automated software engineering (ASE), pp. 349\u2013360. ACM (2014)","DOI":"10.1145\/2642937.2642987"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 1254, pp. 72\u201383. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63166-6_10"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Programming Language Design and Implementation (PLDI), pp. 405\u2013416. ACM (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31612-8_13"},{"issue":"4","key":"18_CR16","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. (CSUR) 41(4), 21 (2009)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1007\/978-3-642-39799-8_59","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2013","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846\u2013862. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_59"},{"key":"18_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s00236-015-0236-z","volume":"53","author":"J Leroux","year":"2016","unstructured":"Leroux, J., R\u00fcmmer, P., Suboti\u0107, P.: Guiding craig interpolation with domain-specific abstractions. Acta Inform. 53, 1\u201338 (2016)","journal-title":"Acta Inform."},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Nori, A.V., Rajamani, S.K.: An empirical study of optimizations in YOGI. In: Software Engineering (ICSE), vol. 1, pp. 355\u2013364. ACM (2010)","DOI":"10.1145\/1806799.1806852"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-39799-8_24","volume-title":"Computer Aided Verification","author":"P R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347\u2013363. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_24"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Sajaniemi, J.: An empirical analysis of roles of variables in novice-level procedural programs. In: Human-Centric Computing Languages and Environments (HCC), pp. 37\u201339. IEEE (2002)","DOI":"10.1109\/HCC.2002.1046340"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Van Deursen, A., Moonen, L.: Type inference for COBOL systems. In: Reverse Engineering (RE), pp. 220\u2013230. IEEE (1998)","DOI":"10.1109\/WCRE.1998.723192"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57288-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T10:29:20Z","timestamp":1498386560000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57288-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319572871","9783319572888"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57288-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}