{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T20:54:50Z","timestamp":1777582490764,"version":"3.51.4"},"publisher-location":"Cham","reference-count":120,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_16","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"493-540","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":40,"title":["Combining Model Checking and Data-Flow Analysis"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sumit","family":"Gulwani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David A.","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A Theory of Objects","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)"},{"key":"16_CR2","volume-title":"Compilers: Principles, Techniques, and Tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)"},{"key":"16_CR3","series-title":"LNCS","first-page":"268","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstractions for model checking C programs. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02031, pp.\u00a0268\u2013283. Springer, Heidelberg (2001)"},{"key":"16_CR4","first-page":"1","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The Slam project: debugging system software via static analysis. In: Launchbury, J., Mitchell, J.C. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a01\u20133. ACM, New York (2002)"},{"key":"16_CR5","unstructured":"Ball, T., Rajamani, S.K.: SLIC: a specification language for interface checking (of C). Tech. Rep. MSR-TR-2001-21, Microsoft Research (2002)"},{"key":"16_CR6","series-title":"LNCS","first-page":"373","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"D. Beyer","year":"2014","unstructured":"Beyer, D.: Status report on software verification (competition summary SV-COMP 2014). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0373\u2013388. Springer, Heidelberg (2014)"},{"key":"16_CR7","first-page":"326","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"D. Beyer","year":"2004","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Finkelstein, A., Estublier, J., Rosenblum, D.S. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0326\u2013335. IEEE, Piscataway (2004)"},{"key":"16_CR8","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/978-3-540-27864-1_2","volume-title":"Intl. Symp. on Static Analysis (SAS)","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.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a03148, pp.\u00a02\u201318. Springer, Heidelberg (2004)"},{"key":"16_CR9","first-page":"25","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"D. Beyer","year":"2009","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a025\u201332. IEEE, Piscataway (2009)"},{"key":"16_CR10","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"D. Beyer","year":"2016","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: Intl. Symp. on Foundations of Software Engineering (FSE). ACM, New York (2016)"},{"key":"16_CR11","first-page":"721","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"D. Beyer","year":"2015","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Nitto, E.D., Harman, M., Heymans, P. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0721\u2013733. ACM, New York (2015)"},{"key":"16_CR12","first-page":"80","volume-title":"Intl. Conf. on Program Comprehension (ICPC)","author":"D. Beyer","year":"2010","unstructured":"Beyer, D., Fararooy, A.: A simple and effective measure for complex low-level dependencies. In: Intl. Conf. on Program Comprehension (ICPC), pp.\u00a080\u201383. IEEE, Piscataway (2010)"},{"issue":"5\u20136","key":"16_CR13","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. Int. J. Softw. Tools Technol. Transf. 9(5\u20136), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"16_CR14","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a04349, pp.\u00a0378\u2013394. Springer, Heidelberg (2007)"},{"key":"16_CR15","first-page":"300","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Ferrante, J., McKinley, K.S. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0300\u2013309. ACM, New York (2007)"},{"key":"16_CR16","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"532","DOI":"10.1007\/11817963_48","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Beyer","year":"2006","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R.B. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a0532\u2013546. Springer, Heidelberg (2006)"},{"key":"16_CR17","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1007\/978-3-540-73368-3_51","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04590, pp.\u00a0504\u2013518. Springer, Heidelberg (2007)"},{"key":"16_CR18","first-page":"29","volume-title":"Intl. Conf. on Automated Software Engineering (ASE)","author":"D. Beyer","year":"2008","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Program analysis with dynamic precision adjustment. In: Intl. Conf. on Automated Software Engineering (ASE), pp.\u00a029\u201338. IEEE, Piscataway (2008)"},{"key":"16_CR19","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/978-3-642-12029-9_19","volume-title":"Intl. Conf. on Fundamental Approaches to Software Engineering (FASE)","author":"D. Beyer","year":"2010","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G., Zufferey, D.: Shape refinement through explicit heap analysis. In: Rosenblum, D.S., Taentzer, G. (eds.) Intl. Conf. on Fundamental Approaches to Software Engineering (FASE). LNCS, vol.\u00a06013, pp.\u00a0263\u2013277. Springer, Heidelberg (2010)"},{"key":"16_CR20","series-title":"LNCS","first-page":"472","volume-title":"European Symp. on Programming (ESOP)","author":"D. Beyer","year":"2013","unstructured":"Beyer, D., Holzer, A., Tautschnig, M., Veith, H.: Information reuse for multi-goal reachability analyses. In: Felleisen, M., Gardner, P. (eds.) European Symp. on Programming (ESOP). LNCS, vol.\u00a07792, pp.\u00a0472\u2013491. Springer, Heidelberg (2013)"},{"key":"16_CR21","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06806, pp.\u00a0184\u2013190. Springer, Heidelberg (2011)"},{"key":"16_CR22","first-page":"189","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"D. Beyer","year":"2010","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Bloem, R., Sharygina, N. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp.\u00a0189\u2013197 (2010)"},{"key":"16_CR23","series-title":"LNCS","volume-title":"Intl. Conf. on Verified Software: Theories, Tools, and Experiments (VSTTE)","author":"D. Beyer","year":"2016","unstructured":"Beyer, D., Lemberger, T.: Symbolic execution with CEGAR. In: Intl. Conf. on Verified Software: Theories, Tools, and Experiments (VSTTE). LNCS. Springer, Heidelberg (2016)"},{"key":"16_CR24","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/978-3-642-37057-1_11","volume-title":"Intl. Conf. on Fundamental Approaches to Software Engineering (FASE)","author":"D. Beyer","year":"2013","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: Cortellessa, V., Varr\u00f3, D. (eds.) Intl. Conf. on Fundamental Approaches to Software Engineering (FASE). LNCS, vol.\u00a07793, pp.\u00a0146\u2013162. Springer, Heidelberg (2013)"},{"key":"16_CR25","series-title":"LNCS","first-page":"1","volume-title":"Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS)","author":"D. Beyer","year":"2013","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software model checking with CPAchecker. In: Kucera, A., Henzinger, T.A., Nesetril, J., Vojnar, T., Antos, D. (eds.) Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS). LNCS, vol.\u00a07721, pp.\u00a01\u201311. Springer, Heidelberg (2013)"},{"key":"16_CR26","series-title":"LNCS","first-page":"1","volume-title":"Intl. Symposium on Model Checking of Software (SPIN)","author":"D. Beyer","year":"2013","unstructured":"Beyer, D., Wendler, P.: Reuse of verification results: conditional model checking, precision reuse, and verification witnesses. In: Bartocci, E., Ramakrishnan, C.R. (eds.) Intl. Symposium on Model Checking of Software (SPIN). LNCS, vol.\u00a07976, pp.\u00a01\u201317. Springer, Heidelberg (2013)"},{"key":"16_CR27","series-title":"LNCS","first-page":"193","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, R. (ed.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01579, pp.\u00a0193\u2013207. Springer, Heidelberg (1999)"},{"key":"16_CR28","first-page":"196","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0196\u2013207. ACM, New York (2003)"},{"key":"16_CR29","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/BFb0039704","volume-title":"Formal Methods in Programming and Their Applications","author":"F. Bourdoncle","year":"1993","unstructured":"Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Bj\u00f8rner, D., Broy, M., Pottosin, I.V. (eds.) Formal Methods in Programming and Their Applications. LNCS, vol.\u00a0735, pp.\u00a0128\u2013141. Springer, Heidelberg (1993)"},{"key":"16_CR30","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/978-3-642-39799-8_28","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"M. Brockschmidt","year":"2013","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a08044, pp.\u00a0413\u2013429. Springer, Heidelberg (2013)"},{"issue":"8","key":"16_CR31","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. Comput. C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"16_CR32","first-page":"289","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"C. Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0289\u2013300. ACM, New York (2009)"},{"key":"16_CR33","first-page":"57","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"S. Chaudhuri","year":"2010","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity analysis of programs. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a057\u201370. ACM, New York (2010)"},{"issue":"5","key":"16_CR34","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. 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":"16_CR35","series-title":"LNCS","first-page":"570","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"E.M. Clarke","year":"2005","unstructured":"Clarke, E.M., Kr\u00f6ning, D., Sharygina, N., Yorav, K.: SatAbs: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a03440, pp.\u00a0570\u2013574. Springer, Heidelberg (2005)"},{"key":"16_CR36","first-page":"194","volume-title":"ACM Workshop on Partial Evaluation and Program Manipulation (PEPM)","author":"M. Codish","year":"1993","unstructured":"Codish, M., Mulkers, A., Bruynooghe, M., de la Banda, M.G., Hermenegildo, M.: Improving abstract interpretations by combining domains. In: ACM Workshop on Partial Evaluation and Program Manipulation (PEPM), pp.\u00a0194\u2013205. ACM, New York (1993)"},{"key":"16_CR37","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990)"},{"key":"16_CR38","first-page":"238","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0238\u2013252. ACM, New York (1977)"},{"key":"16_CR39","first-page":"269","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program-analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0269\u2013282. ACM, New York (1979)"},{"key":"16_CR40","first-page":"170","volume-title":"Intl. Conf. on Functional Programming Languages and Computer Architecture (FPCA)","author":"P. Cousot","year":"1995","unstructured":"Cousot, P., Cousot, R.: Formal language, grammar, and set-constraint-based program analysis by abstract interpretation. In: Intl. Conf. on Functional Programming Languages and Computer Architecture (FPCA), pp.\u00a0170\u2013181. ACM, New York (1995)"},{"key":"16_CR41","first-page":"84","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a084\u201396. ACM, New York (1978)"},{"issue":"3","key":"16_CR42","doi-asserted-by":"crossref","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 (1957)","journal-title":"J. Symb. Log."},{"key":"16_CR43","first-page":"207","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"L. Damas","year":"1982","unstructured":"Damas, L., Milner, R.: Principal type schemes for functional languages. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0207\u2013212. ACM, New York (1982)"},{"key":"16_CR44","series-title":"LNCS","first-page":"138","volume-title":"Intl. Symp. on Formal Methods for Components and Objects (FMCO)","author":"D. Dams","year":"2005","unstructured":"Dams, D., Namjoshi, K.S.: Orion: high-precision methods for static error analysis of C and C++ programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) Intl. Symp. on Formal Methods for Components and Objects (FMCO). LNCS, vol.\u00a04111, pp.\u00a0138\u2013160. Springer, Heidelberg (2005)"},{"key":"16_CR45","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/978-3-642-38856-9_13","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"K. Dudka","year":"2013","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a07935, pp.\u00a0215\u2013237. Springer, Heidelberg (2013)"},{"key":"16_CR46","series-title":"LNCS","first-page":"412","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"K. Dudka","year":"2014","unstructured":"Dudka, K., Peringer, P., Vojnar, T.: Predator: a shape analyzer based on symbolic memory graphs (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0412\u2013414. Springer, Heidelberg (2014)"},{"key":"16_CR47","series-title":"LNCS","first-page":"421","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"E. Ermis","year":"2014","unstructured":"Ermis, E., Nutz, A., Dietsch, D., Hoenicke, J., Podelski, A.: Ultimate Kojak (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0421\u2013423. Springer, Heidelberg (2014)"},{"key":"16_CR48","series-title":"LNCS","first-page":"623","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Falke","year":"2013","unstructured":"Falke, S., Merz, F., Sinz, C.L.: Improved bounded model checking of C programs using LLVM (competition contribution). In: Piterman, N., Smolka, S.A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a07795, pp.\u00a0623\u2013626. Springer, Heidelberg (2013)"},{"key":"16_CR49","first-page":"227","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"J. Fischer","year":"2005","unstructured":"Fischer, J., Jhala, R., Majumdar, R.: Joining data flow with predicates. In: Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0227\u2013236. ACM, New York (2005)"},{"key":"16_CR50","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/3-540-61053-7_56","volume-title":"Intl. Conf. on Compiler Construction (CC)","author":"A. Geser","year":"1996","unstructured":"Geser, A., Knoop, J., L\u00fcttgen, G., R\u00fcthing, O., Steffen, B.: Non-monotone fixpoint iterations to resolve second-order effects. In: Gyim\u00f3thy, T. (ed.) Intl. Conf. on Compiler Construction (CC). LNCS, vol.\u00a01060, pp.\u00a0106\u2013120. Springer, Heidelberg (1996)"},{"key":"16_CR51","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Intl. Joint Conf. on Automated Reasoning (IJCAR)","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR). LNAI, vol.\u00a04130, pp.\u00a0281\u2013286. Springer, Heidelberg (2006)"},{"key":"16_CR52","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with Pvs. In: Grumberg, O. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01254, pp.\u00a072\u201383. Springer, Heidelberg (1997)"},{"key":"16_CR53","first-page":"277","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"S. Gulwani","year":"2007","unstructured":"Gulwani, S., Jojic, N.: Program verification as probabilistic inference. In: Hofmann, M., Felleisen, M. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0277\u2013289. ACM, New York (2007)"},{"key":"16_CR54","unstructured":"Gulwani, S., Juvekar, S.: Bound analysis using backward symbolic execution. Tech. Rep. MSR-TR-2009-156, Microsoft Research (2009)"},{"key":"16_CR55","first-page":"239","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: Shao, Z., Pierce, B.C. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0239\u2013251. ACM, New York (2009)"},{"key":"16_CR56","first-page":"235","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Necula, G.C., Wadler, P. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0235\u2013246. ACM, New York (2008)"},{"key":"16_CR57","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/978-3-540-27864-1_17","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"S. Gulwani","year":"2004","unstructured":"Gulwani, S., Necula, G.C.: A polynomial-time algorithm for global value numbering. In: Giacobazzi, R. (ed.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a03148, pp.\u00a0212\u2013227. Springer, Heidelberg (2004)"},{"key":"16_CR58","first-page":"281","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Gupta, R., Amarasinghe, S.P. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0281\u2013292. ACM, New York (2008)"},{"key":"16_CR59","series-title":"LNCS","first-page":"120","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","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.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a05403, pp.\u00a0120\u2013135. Springer, Heidelberg (2009)"},{"key":"16_CR60","series-title":"LNCS","first-page":"279","volume-title":"European Symp. on Programming (ESOP)","author":"S. Gulwani","year":"2006","unstructured":"Gulwani, S., Tiwari, A.: Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In: Sestoft, P. (ed.) European Symp. on Programming (ESOP). LNCS, vol.\u00a03924, pp.\u00a0279\u2013293. Springer, Heidelberg (2006)"},{"key":"16_CR61","first-page":"376","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"S. Gulwani","year":"2006","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Schwartzbach, M.I., Ball, T. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0376\u2013386. ACM, New York (2006)"},{"key":"16_CR62","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/978-3-540-69738-1_26","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"S. Gulwani","year":"2007","unstructured":"Gulwani, S., Tiwari, A.: Assertion checking unified. In: Cook, B., Podelski, A. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a04349, pp.\u00a0363\u2013377. Springer, Heidelberg (2007)"},{"key":"16_CR63","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/978-3-540-70545-1_18","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a05123, pp.\u00a0190\u2013203. Springer, Heidelberg (2008)"},{"key":"16_CR64","first-page":"292","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"S. Gulwani","year":"2010","unstructured":"Gulwani, S., Zuleger, F.: The reachability-bound problem. In: Zorn, B.G., Aiken, A. (eds.) Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0292\u2013304. ACM, New York (2010)"},{"key":"16_CR65","series-title":"LNCS","first-page":"637","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Gurfinkel","year":"2013","unstructured":"Gurfinkel, A., Albarghouthi, A., Chaki, S., Li, Y., Chechik, M.U.: Verification with interpolants and abstract interpretation (competition contribution). In: Piterman, N., Smolka, S.A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a07795, pp.\u00a0637\u2013640. Springer, Heidelberg (2013)"},{"key":"16_CR66","series-title":"LNCS","first-page":"408","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"A. Gurfinkel","year":"2014","unstructured":"Gurfinkel, A., Belov, A.: FrankenBit: bit-precise verification with many bits (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0408\u2013411. Springer, Heidelberg (2014)"},{"key":"16_CR67","series-title":"LNCS","first-page":"418","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M. Heizmann","year":"2014","unstructured":"Heizmann, M., Christ, J., Dietsch, D., Hoenicke, J., Lindenmann, M., Musa, B., Schilling, C., Wissert, S., Podelski, A.: Ultimate Automizer with unsatisfiable cores (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0418\u2013420. Springer, Heidelberg (2014)"},{"key":"16_CR68","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/978-3-319-02444-8_26","volume-title":"Intl. Symp. Automated Technology for Verification and Analysis (ATVA)","author":"M. Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Hung, D.V., Ogawa, M. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol.\u00a08172, pp.\u00a0365\u2013380. Springer, Heidelberg (2013)"},{"key":"16_CR69","first-page":"232","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0232\u2013244. ACM, New York (2004)"},{"key":"16_CR70","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02404, pp.\u00a0526\u2013538. Springer, Heidelberg (2002)"},{"key":"16_CR71","first-page":"58","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Launchbury, J., Mitchell, J.C. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a058\u201370. ACM, New York (2002)"},{"key":"16_CR72","series-title":"LNCS","first-page":"398","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"O. Inverso","year":"2014","unstructured":"Inverso, O., Tomasco, E., Fischer, B., Torre, S.L., Parlato, G.: Lazy-CSeq: a lazy sequentialization tool for C (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0398\u2013401. Springer, Heidelberg (2014)"},{"key":"16_CR73","series-title":"LNCS","first-page":"423","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K. Johannes","year":"2008","unstructured":"Johannes, K., Helmut, V.: Jakstab: a static analysis platform for binaries. In: Gupta, A., Malik, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a05123, pp.\u00a0423\u2013427. Springer, Heidelberg (2008)"},{"key":"16_CR74","first-page":"215","volume-title":"Intl. Conf. on Software Engineering (ICSE)","author":"S. Jha","year":"2010","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Kramer, J., Bishop, J., Devanbu, P.T., Uchitel, S. (eds.) Intl. Conf. on Software Engineering (ICSE), pp.\u00a0215\u2013224. ACM, New York (2010)"},{"key":"16_CR75","first-page":"66","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"N.D. Jones","year":"1982","unstructured":"Jones, N.D., Muchnick, S.S.: A flexible approach to interprocedural data-flow analysis and programs with recursive data structures. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a066\u201374. ACM, New York (1982)"},{"key":"16_CR76","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/978-3-642-11319-2_15","volume-title":"Intl. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI)","author":"Y. Jung","year":"2010","unstructured":"Jung, Y., Kong, S., Wang, B.Y., Yi, K.: Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction. In: Barthe, G., Hermenegildo, M.V. (eds.) Intl. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol.\u00a05944, pp.\u00a0180\u2013196. Springer, Heidelberg (2010)"},{"issue":"1","key":"16_CR77","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1145\/321921.321938","volume":"23","author":"J. Kam","year":"1976","unstructured":"Kam, J., Ullman, J.: Global data-flow analysis and iterative algorithms. J. ACM 23(1), 158\u2013171 (1976)","journal-title":"J. ACM"},{"key":"16_CR78","first-page":"5","volume-title":"Program Flow Analysis: Theory and Applications","author":"K. Kennedy","year":"1981","unstructured":"Kennedy, K.: A survey of data-flow analysis techniques. In: Jones, N.D., Muchniek, S.S. (eds.) Program Flow Analysis: Theory and Applications, pp.\u00a05\u201354. Prentice Hall, New York (1981)"},{"key":"16_CR79","series-title":"LNCS","first-page":"422","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M. Klein","year":"1996","unstructured":"Klein, M., Knoop, J., Kosch\u00fctzki, D., Steffen, B.: DFA&OPT-METAFrame: a tool kit for program analysis and optimization. In: Margaria, T., Steffen, B. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01055, pp.\u00a0422\u2013426. Springer, Heidelberg (1996)"},{"issue":"4","key":"16_CR80","first-page":"211","volume":"4","author":"J. Knoop","year":"1996","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Towards a tool kit for the automatic generation of interprocedural data-flow analyses. J. Program. Lang. 4(4), 211\u2013246 (1996)","journal-title":"J. Program. Lang."},{"key":"16_CR81","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"J. Knoop","year":"1992","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Lazy code motion. In: Conf. on Programming Language Design and Implementation (PLDI). ACM, New York (1992)"},{"issue":"2","key":"16_CR82","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/BF01692511","volume":"2","author":"D.E. Knuth","year":"1968","unstructured":"Knuth, D.E.: Semantics of context-free languages. Math. Syst. Theory 2(2), 127\u2013145 (1968)","journal-title":"Math. Syst. Theory"},{"key":"16_CR83","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/978-3-642-17164-2_23","volume-title":"Asian Symp. on Programming Languages and Systems (APLAS)","author":"S. Kong","year":"2010","unstructured":"Kong, S., Jung, Y., David, C., Wang, B.Y., Yi, K.: Automatically inferring quantified invariants via algorithmic learning from simple templates. In: Ueda, K. (ed.) Asian Symp. on Programming Languages and Systems (APLAS). LNCS, vol.\u00a06461, pp.\u00a0328\u2013343 (2010)"},{"key":"16_CR84","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/978-3-642-14295-6_9","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D. Kr\u00f6ning","year":"2010","unstructured":"Kr\u00f6ning, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06174, pp.\u00a089\u2013103. Springer, Heidelberg (2010)"},{"key":"16_CR85","series-title":"LNCS","first-page":"389","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"D. Kr\u00f6ning","year":"2014","unstructured":"Kr\u00f6ning, D., Tautschnig, M.: CBMC: C bounded model checker (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0389\u2013391. Springer, Heidelberg (2014)"},{"key":"16_CR86","volume-title":"Compiler Design Theory","author":"P. Lewis","year":"1976","unstructured":"Lewis, P., Rosenkrantz, D., Stearns, R.: Compiler Design Theory. Addison-Wesley, Reading (1976)"},{"key":"16_CR87","series-title":"LNCS","first-page":"392","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. L\u00f6we","year":"2014","unstructured":"L\u00f6we, S., Mandrykin, M., Wendler, P.: CPAchecker with sequential combination of explicit-value analyses and predicate analyses (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0392\u2013394. Springer, Heidelberg (2014)"},{"key":"16_CR88","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/3-540-45937-5_6","volume-title":"Intl. Conf. on Compiler Construction (CC)","author":"M. Mohnen","year":"2002","unstructured":"Mohnen, M.: A graph-free approach to data-flow analysis. In: Horspool, R.N. (ed.) Intl. Conf. on Compiler Construction (CC). LNCS, vol.\u00a02304, pp.\u00a046\u201361. Springer, Heidelberg (2002)"},{"issue":"2","key":"16_CR89","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1145\/359060.359069","volume":"22","author":"E. Morel","year":"1979","unstructured":"Morel, E., Renvoise, C.: Global optimization by suppression of partial redundancies. Commun. ACM 22(1) (1979)","journal-title":"Communications of the ACM"},{"key":"16_CR90","series-title":"LNCS","first-page":"405","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"J. Morse","year":"2014","unstructured":"Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B.: ESBMC 1.22 (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0405\u2013407. Springer, Heidelberg (2014)"},{"key":"16_CR91","series-title":"LNCS","first-page":"395","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"P. Muller","year":"2014","unstructured":"Muller, P., Vojnar, T.: CPAlien: shape analyzer for CPAchecker (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0395\u2013397. Springer, Heidelberg (2014)"},{"key":"16_CR92","first-page":"330","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Jones, N.D., Leroy, X. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0330\u2013341. ACM, New York (2004)"},{"key":"16_CR93","series-title":"LNCS","first-page":"217","volume-title":"European Symp. on Programming (ESOP)","author":"A. Mycroft","year":"1984","unstructured":"Mycroft, A.: Polymorphic type schemes and recursive definitions. In: Paul, M., Robinet, B. (eds.) European Symp. on Programming (ESOP). LNCS, vol.\u00a0167, pp.\u00a0217\u2013228. Springer, Heidelberg (1984)"},{"key":"16_CR94","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)"},{"key":"16_CR95","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Programming in Martin-L\u00f6f\u2019s Type Theory. Oxford University Press, Oxford (1990)"},{"key":"16_CR96","series-title":"LNCS","first-page":"284","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"C.S. Pasareanu","year":"2001","unstructured":"Pasareanu, C.S., Dwyer, M.B., Visser, W.: Finding feasible counter-examples when model checking abstracted Java programs. In: Margaria, T., Yi, W. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a02031, pp.\u00a0284\u2013298. Springer, Heidelberg (2001)"},{"key":"16_CR97","volume-title":"Types and Programming Languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"16_CR98","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a02937, pp.\u00a0239\u2013251. Springer, Heidelberg (2004)"},{"key":"16_CR99","series-title":"LNCS","first-page":"633","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"C. Popeea","year":"2013","unstructured":"Popeea, C., Rybalchenko, A.: Threader: a verifier for multi-threaded programs (competition contribution). In: Piterman, N., Smolka, S.A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a07795, pp.\u00a0633\u2013636. Springer, Heidelberg (2013)"},{"key":"16_CR100","first-page":"49","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"T.W. Reps","year":"1995","unstructured":"Reps, T.W., Horwitz, S., Sagiv, M.: Precise interprocedural data-flow analysis via graph reachability. In: Cytron, R.K., Lee, P. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a049\u201361. ACM, New York (1995)"},{"key":"16_CR101","first-page":"12","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"B.K. Rosen","year":"1988","unstructured":"Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a012\u201327. ACM, New York (1988)"},{"issue":"8","key":"16_CR102","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1109\/32.536955","volume":"22","author":"G. Rothermel","year":"1996","unstructured":"Rothermel, G., Harrold, M.: Analyzing regression test selection techniques. IEEE Trans. Softw. Eng. 22(8), 529\u2013551 (1996)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"16_CR103","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR104","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-540-27864-1_7","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a03148, pp.\u00a053\u201368. Springer, Heidelberg (2004)"},{"key":"16_CR105","first-page":"318","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0318\u2013329. ACM, New York (2004)"},{"key":"16_CR106","volume-title":"Denotational Semantics: A Methodology for Language Development","author":"D.A. Schmidt","year":"1986","unstructured":"Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. Allyn & Bacon, Needham Heights (1986)"},{"key":"16_CR107","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"D.A. Schmidt","year":"1998","unstructured":"Schmidt, D.A.: Data-flow analysis is model checking of abstract interpretations. In: Symp. on Principles of Programming Languages (POPL). ACM, New York (1998)"},{"key":"16_CR108","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"D.A. Schmidt","year":"1998","unstructured":"Schmidt, D.A., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a01503, pp.\u00a0351\u2013380. Springer, Heidelberg (1998)"},{"key":"16_CR109","series-title":"LNCS","first-page":"525","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"P. Shved","year":"2012","unstructured":"Shved, P., Mandrykin, M., Mutilin, V.: Predicate analysis with Blast 2.7 (competition contribution). In: Flanagan, C., K\u00f6nig, B. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a07214, pp.\u00a0525\u2013527. Springer, Heidelberg (2012)"},{"key":"16_CR110","series-title":"LNCS","first-page":"415","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"J. Slaby","year":"2014","unstructured":"Slaby, J., Strejcek, J.: Symbiotic 2: more precise slicing (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0415\u2013417. Springer, Heidelberg (2014)"},{"key":"16_CR111","first-page":"223","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"S. Srivastava","year":"2009","unstructured":"Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0223\u2013234. ACM, New York (2009)"},{"key":"16_CR112","first-page":"313","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"S. Srivastava","year":"2010","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: Hermenegildo, M.V., Palsberg, J. (eds.) Symp. on Principles of Programming Languages (POPL), pp.\u00a0313\u2013326. ACM, New York (2010)"},{"key":"16_CR113","series-title":"LNCS","first-page":"346","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"B. Steffen","year":"1991","unstructured":"Steffen, B.: Data-flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a0536, pp.\u00a0346\u2013365. Springer, Heidelberg (1991)"},{"issue":"2","key":"16_CR114","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0167-6423(93)90003-8","volume":"21","author":"B. Steffen","year":"1993","unstructured":"Steffen, B.: Generating data-flow analysis algorithms from modal specifications. Sci. Comput. Program. 21(2), 115\u2013139 (1993)","journal-title":"Sci. Comput. Program."},{"key":"16_CR115","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/3-540-61739-6_31","volume-title":"Intl. Symp. on Static Analysis (SAS)","author":"B. Steffen","year":"1996","unstructured":"Steffen, B.: Property-oriented expansion. In: Cousot, R., Schmidt, D.A. (eds.) Intl. Symp. on Static Analysis (SAS). LNCS, vol.\u00a01145, pp.\u00a022\u201341. Springer, Heidelberg (1996)"},{"key":"16_CR116","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-60218-6_6","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"B. Steffen","year":"1995","unstructured":"Steffen, B., Cla\u00dfen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a0962, pp.\u00a072\u201387. Springer, Heidelberg (1995)"},{"key":"16_CR117","series-title":"LNCS","first-page":"402","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"E. Tomasco","year":"2014","unstructured":"Tomasco, E., Inverso, O., Fischer, B., Torre, S.L., Parlato, G.: MU-CSeq: sequentialization of C programs by shared memory unwindings (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a08413, pp.\u00a0402\u2013404. Springer, Heidelberg (2014)"},{"key":"16_CR118","series-title":"LNCS","first-page":"412","volume-title":"European Symp. on Programming (ESOP)","author":"C. Urban","year":"2014","unstructured":"Urban, C., Min\u00e9, A.: An abstract domain to infer ordinal-valued ranking functions. In: Shao, Z. (ed.) European Symp. on Programming (ESOP). LNCS, vol.\u00a08410, pp.\u00a0412\u2013431. Springer, Heidelberg (2014)"},{"key":"16_CR119","series-title":"LNCS","first-page":"308","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Y. Vizel","year":"2013","unstructured":"Vizel, Y., Grumberg, O., Shoham, S.: Intertwined forward-backward reachability analysis using interpolants. In: Piterman, N., Smolka, S.A. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a07795, pp.\u00a0308\u2013323. Springer, Heidelberg (2013)"},{"key":"16_CR120","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/978-3-642-00593-0_32","volume-title":"Intl. Conf. on Fundamental Approaches to Software Engineering (FASE)","author":"O. \u0160er\u00fd","year":"2009","unstructured":"\u0160er\u00fd, O.: Enhanced property specification and verification in Blast. In: Chechik, M., Wirsing, M. (eds.) Intl. Conf. on Fundamental Approaches to Software Engineering (FASE). LNCS, vol.\u00a05503, pp.\u00a0456\u2013469. Springer, Heidelberg (2009)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T05:44:49Z","timestamp":1571377489000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":120,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_16","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}