{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T04:34:11Z","timestamp":1747888451413,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466742"},{"type":"electronic","value":"9783662466759"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46675-9_13","type":"book-chapter","created":{"date-parts":[[2015,3,31]],"date-time":"2015-03-31T20:24:38Z","timestamp":1427833478000},"page":"186-201","source":"Crossref","is-referenced-by-count":8,"title":["Symbolic Detection of Assertion Dependencies for Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Grigory","family":"Fedyukovich","sequence":"first","affiliation":[]},{"given":"Andrea Callia","family":"D\u2019Iddio","sequence":"additional","affiliation":[]},{"given":"Antti E. J.","family":"Hyv\u00e4rinen","sequence":"additional","affiliation":[]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-12002-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The openSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 150\u2013153. Springer, Heidelberg (2010)"},{"key":"13_CR3","first-page":"1417","volume-title":"DATE 2013","author":"G. Cabodi","year":"2013","unstructured":"Cabodi, G., Lolacono, C., Vendraminetto, D.: Optimization techniques for Craig interpolant compaction in unbounded model checking. In: DATE 2013, pp. 1417\u20131422. ACM DL, EDA Consortium San Jose (2013)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, A.: Synthesis of Synchronization Skeletons for Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, Springer, Heidelberg (1982)"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Cobb, J., Jones, J.A., Kapfhammer, G.M., Harrold, M.J.: Dynamic invariant detection for relational databases. In: Proc.\u00a0International Workshop on Dynamic Analysis 2011, pp. 12\u201317. ACM (2011)","DOI":"10.1145\/2002951.2002955"},{"issue":"3","key":"13_CR7","first-page":"269","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Genzen theorem in relating model theory and proof theory. JSL\u00a022(3), 269\u2013285 (1957)","journal-title":"JSL"},{"key":"13_CR8","unstructured":"Dodoo, N., Donovan, A., Lin, L., Ernst, M.D.: Selecting predicates for implications in program analysis (2002), http:\/\/homes.cs.washington.edu\/~mernst\/pubs\/invariants-implications.ps"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-12002-2_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A.F. Donaldson","year":"2010","unstructured":"Donaldson, A.F., Kroening, D., R\u00fcmmer, P.: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 280\u2013295. Springer, Heidelberg (2010)"},{"issue":"2","key":"13_CR10","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1109\/32.908957","volume":"27","author":"M.D. Ernst","year":"2001","unstructured":"Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering\u00a027(2), 99\u2013123 (2001)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-642-36742-7_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Fedyukovich","year":"2013","unstructured":"Fedyukovich, G., Sery, O., Sharygina, N.: eVolCheck: Incremental Upgrade Checker for C. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 292\u2013307. Springer, Heidelberg (2013)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-319-15075-8_7","volume-title":"Formal Methods: Foundations and Applications","author":"G. Fedyukovich","year":"2015","unstructured":"Fedyukovich, G., Sharygina, N.: Towards Completeness in Bounded Model Checking Through Automatic Recursion Depth Detection. In: Braga, C., Mart\u00ed-Oliet, N. (eds.) SBMF 2014. LNCS, vol.\u00a08941, pp. 96\u2013112. Springer, Heidelberg (2015)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Rustan, K., Leino, M.: Houdini, an annotation assistant for eSC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"issue":"3","key":"13_CR14","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1016\/j.tcs.2008.03.013","volume":"404","author":"F. Ivancic","year":"2008","unstructured":"Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. TCS\u00a0404(3), 256\u2013274 (2008)","journal-title":"TCS"},{"issue":"3","key":"13_CR15","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10703-012-0176-y","volume":"42","author":"D. Kroening","year":"2013","unstructured":"Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using state and transition invariants. Formal Methods in System Design\u00a042(3), 221\u2013261 (2013)","journal-title":"Formal Methods in System Design"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S.: A program transformation for faster goal-directed search. In: Proc.\u00a0FMCAD 2014, pp. 147\u2013154. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987607"},{"issue":"4","key":"13_CR17","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1109\/TSE.2010.93","volume":"37","author":"L. Mariani","year":"2011","unstructured":"Mariani, L., Pastore, F., Pezz\u00e8, M.: Dynamic analysis for diagnosing integration faults. IEEE Transactions on Software Engineering\u00a037(4), 486\u2013508 (2011)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-27705-4_12","volume-title":"Verified Software: Theories, Tools, Experiments","author":"F. Merz","year":"2012","unstructured":"Merz, F., Falke, S., Sinz, C.: LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 146\u2013161. Springer, Heidelberg (2012)"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: Proc.\u00a0ICSE 2012, pp. 683\u2013693. IEEE (2012)","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Pastore, F., Mariani, L., Hyv\u00e4rinen, A.E.J., Fedyukovich, G., Sharygina, N., Sehestedt, S., Muhammad, A.: Verification-aided regression testing. In: Proc.\u00a0ISSTA 2014, pp. 37\u201348. ACM (2014)","DOI":"10.1145\/2610384.2610387"},{"issue":"3","key":"13_CR21","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic\u00a062(3), 981\u2013998 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.-P. Queille","year":"1982","unstructured":"Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1007\/978-3-642-45221-5_45","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S.F. Rollini","year":"2013","unstructured":"Rollini, S.F., Alt, L., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: PeRIPLO: A framework for producing effective interpolants in SAT-based software verification. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol.\u00a08312, pp. 683\u2013693. Springer, Heidelberg (2013)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-33386-6_17","volume-title":"Automated Technology for Verification and Analysis","author":"O. Sery","year":"2012","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: FunFrog: Bounded model checking with interpolation-based function summarization. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 203\u2013207. Springer, Heidelberg (2012)"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Weiser, M.: Program slicing. In: Proc.\u00a0ICSE 1981, pp. 439\u2013449. IEEE (1981)","DOI":"10.1149\/198109.0439PV"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Yang, G., Khurshid, S., Person, S., Rungta, N.: Property differencing for incremental checking. In: Proc.\u00a0ICSE 2014, pp. 1059\u20131070. ACM (2014)","DOI":"10.1145\/2568225.2568319"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46675-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:47:50Z","timestamp":1747856870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46675-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466742","9783662466759"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46675-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}