{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T00:19:55Z","timestamp":1769732395056,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961415","type":"print"},{"value":"9783319961422","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:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96142-2_5","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T15:55:08Z","timestamp":1532102108000},"page":"37-44","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability"],"prefix":"10.1007","author":[{"given":"Jianwen","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rohit","family":"Dureja","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"5_CR1","unstructured":"AIGER Tools. http:\/\/fmv.jku.at\/aiger\/aiger-1.9.9.tar.gz"},{"key":"5_CR2","unstructured":"HWMCC 2015. http:\/\/fmv.jku.at\/hwmcc15\/"},{"key":"5_CR3","unstructured":"HWMCC 2017. http:\/\/fmv.jku.at\/hwmcc17\/"},{"key":"5_CR4","unstructured":"IC3Ref. https:\/\/github.com\/arbrad\/IC3ref"},{"key":"5_CR5","unstructured":"SimpleCAR Source. https:\/\/github.com\/lijwen2748\/simplecar\/releases\/tag\/v0.1"},{"key":"5_CR6","unstructured":"SimpleCAR Website. http:\/\/temporallogic.org\/research\/CAV18\/"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/11560548_20","volume-title":"Correct Hardware Design and Verification Methods","author":"N Amla","year":"2005","unstructured":"Amla, N., Du, X., Kuehlmann, A., Kurshan, R.P., McMillan, K.L.: An analysis of SAT-based model checking techniques in an industrial environment. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 254\u2013268. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11560548_20"},{"key":"5_CR8","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. In: IJCAI (2009)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Bernardini, A., Ecker, W., Schlichtmann, U.: Where formal verification can help in functional safety analysis. In: ICCAD (2016)","DOI":"10.1145\/2966986.2980087"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs (1999)","DOI":"10.21236\/ADA360973"},{"key":"5_CR11","unstructured":"Biere, A.: AIGER Format. http:\/\/fmv.jku.at\/aiger\/FORMAT"},{"key":"5_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). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"5_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). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"5_CR14","unstructured":"Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: FMCAD (2011)"},{"key":"5_CR15","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). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Golnari, A., Vizel, Y., Malik, S.: Error-tolerant processors: formal specification and verification. In: ICCAD (2015)","DOI":"10.1109\/ICCAD.2015.7372582"},{"issue":"6","key":"5_CR17","doi-asserted-by":"crossref","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":"5_CR18","doi-asserted-by":"crossref","unstructured":"Ivrii, A., Gurfinkel, A.: Pushing to the top. In: FMCAD (2015)","DOI":"10.1109\/FMCAD.2015.7542254"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Li, J., Zhu, S., Zhang, Y., Pu, G., Vardi, M.Y.: Safety model checking with complementary approximations. In: ICCAD (2017)","DOI":"10.1109\/ICCAD.2017.8203765"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-642-21581-0_14","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"J Marques-Silva","year":"2011","unstructured":"Marques-Silva, J., Lynce, I.: On improving MUS extraction algorithms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 159\u2013173. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21581-0_14"},{"key":"5_CR21","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). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"5_CR22","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). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_17"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Yu, Y., Subramanyan, P., Tsiskaridze, N., Malik, S.: All-SAT using minimal blocking clauses. In: VLSID (2014)","DOI":"10.1109\/VLSID.2014.22"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96142-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T23:20:29Z","timestamp":1571613629000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96142-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961415","9783319961422"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96142-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}