{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T09:09:30Z","timestamp":1775898570194,"version":"3.50.1"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030415990","type":"print"},{"value":"9783030416003","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","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":[[2020]]},"DOI":"10.1007\/978-3-030-41600-3_12","type":"book-chapter","created":{"date-parts":[[2020,3,13]],"date-time":"2020-03-13T05:32:04Z","timestamp":1584077524000},"page":"180-192","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Intersection and Rotation of Assumption Literals Boosts Bug-Finding"],"prefix":"10.1007","author":[{"given":"Rohit","family":"Dureja","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianwen","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kristin Y.","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,3,14]]},"reference":[{"key":"12_CR1","unstructured":"AIGER Tools. \nhttp:\/\/fmv.jku.at\/aiger\/aiger-1.9.9.tar.gz"},{"key":"12_CR2","unstructured":"HWMCC 2015. \nhttp:\/\/fmv.jku.at\/hwmcc15\/"},{"key":"12_CR3","unstructured":"HWMCC 2017. \nhttp:\/\/fmv.jku.at\/hwmcc17\/"},{"key":"12_CR4","unstructured":"IC3Ref. \nhttps:\/\/github.com\/arbrad\/IC3ref"},{"key":"12_CR5","unstructured":"Minisat 2.2.0. \nhttps:\/\/github.com\/niklasso\/minisat"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Bernardini, A., Ecker, W., Schlichtmann, U.: Where formal verification can help in functional safety analysis. In: 2016 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp. 1\u20138 (November 2016)","DOI":"10.1145\/2966986.2980087"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Berryhill, R., Ivrii, A., Veira, N., Veneris, A.: Learning support sets in IC3 and Quip: the good, the bad, and the ugly. In: Formal Methods in Computer Aided Design (FMCAD), pp. 140\u2013147 (October 2017)","DOI":"10.23919\/FMCAD.2017.8102252"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using sat procedures instead of BDDs (1999). \nhttps:\/\/doi.org\/10.1145\/309847.309942","DOI":"10.1145\/309847.309942"},{"key":"12_CR9","unstructured":"Biere, A.: AIGER Format. \nhttp:\/\/fmv.jku.at\/aiger\/FORMAT"},{"key":"12_CR10","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 and 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. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: Formal Methods in Computer Aided Design (FMCAD 2007), pp. 173\u2013180 (November 2007)","DOI":"10.1109\/FAMCAD.2007.15"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"issue":"1","key":"12_CR14","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s10703-017-0272-0","volume":"50","author":"G Cabodi","year":"2017","unstructured":"Cabodi, G., Camurati, P.E., Mishchenko, A., Palena, M., Pasini, P.: Sat solver management strategies in IC3: an experimental approach. Formal Methods Syst. Des. 50(1), 39\u201374 (2017). \nhttps:\/\/doi.org\/10.1007\/s10703-017-0272-0","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"12_CR15","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W Dowling","year":"1984","unstructured":"Dowling, W., Gallier, J.: Linear-time algorithms for testing the satisfiability of propositional horn formulae. J. Logic Program. 1(3), 267\u2013284 (1984)","journal-title":"J. Logic Program."},{"key":"12_CR16","unstructured":"Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011, pp. 125\u2013134. FMCAD Inc., Austin (2011). \nhttp:\/\/dl.acm.org\/citation.cfm?id=2157654.2157675"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Golnari, A., Vizel, Y., Malik, S.: Error-tolerant processors: formal specification and verification. In: IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp. 286\u2013293 (November 2015)","DOI":"10.1109\/ICCAD.2015.7372582"},{"issue":"6","key":"12_CR19","doi-asserted-by":"publisher","first-page":"1026","DOI":"10.1109\/TCAD.2015.2481869","volume":"35","author":"A Griggio","year":"2016","unstructured":"Griggio, A., Roveri, M.: Comparing different variants of the IC3 algorithm for hardware model checking. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 35(6), 1026\u20131039 (2016)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Hassan, Z., Bradley, A.R., Somenzi, F.: Better generalization in IC3. In: Formal Methods in Computer-Aided Design, pp. 157\u2013164 (October 2013)","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"12_CR21","unstructured":"Ivrii, A., Gurfinkel, A.: Pushing to the top. In: Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015, pp. 65\u201372, FMCAD Inc., Austin (2015). \nhttp:\/\/dl.acm.org\/citation.cfm?id=2893529.2893545"},{"issue":"4","key":"12_CR22","doi-asserted-by":"publisher","first-page":"21:1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1\u201321:54 (2009). \nhttps:\/\/doi.org\/10.1145\/1592434.1592438","journal-title":"ACM Comput. Surv."},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-319-96142-2_5","volume-title":"Computer Aided Verification","author":"J Li","year":"2018","unstructured":"Li, J., Dureja, R., Pu, G., Rozier, K.Y., Vardi, M.Y.: SimpleCAR: an efficient bug-finding tool based on approximate reachability. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 37\u201344. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-96142-2_5"},{"key":"12_CR24","unstructured":"Li, J., Zhu, S., Zhang, Y., Pu, G., Vardi, M.Y.: Safety model checking with complementary approximations. In: Proceedings of the 36th International Conference on Computer-Aided Design, ICCAD 2017, pp. 95\u2013100. IEEE Press, Piscataway (2017). \nhttp:\/\/dl.acm.org\/citation.cfm?id=3199700.3199713"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, pp. 530\u2013535 (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-319-08867-9_17","volume-title":"Computer Aided Verification","author":"Y Vizel","year":"2014","unstructured":"Vizel, Y., Gurfinkel, A.: Interpolating property directed reachability. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 260\u2013276. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_17"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools, and Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-41600-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,13]],"date-time":"2020-03-13T05:33:58Z","timestamp":1584077638000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-41600-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030415990","9783030416003"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-41600-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 March 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sri-csl.github.io\/VSTTE19\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}