{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T15:51:16Z","timestamp":1778082676945,"version":"3.51.4"},"reference-count":20,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"funder":[{"name":"Partenariato Esteso-RESTART \u201cRESearch and innovation on future Telecommunications systems and networks, to make Italy more smART\u201d","award":["PE00000001"],"award-info":[{"award-number":["PE00000001"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2024]]},"DOI":"10.1109\/access.2024.3446802","type":"journal-article","created":{"date-parts":[[2024,8,21]],"date-time":"2024-08-21T23:38:17Z","timestamp":1724283497000},"page":"119341-119349","source":"Crossref","is-referenced-by-count":1,"title":["Improving Bounded Model Checking Exploiting Interpolation-Based Learning and Strengthening"],"prefix":"10.1109","volume":"12","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5839-8697","authenticated-orcid":false,"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[{"name":"DAUIN-Department of Control and Computer Engineering, Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2476-2160","authenticated-orcid":false,"given":"Paolo","family":"Enrico Camurati","sequence":"additional","affiliation":[{"name":"DAUIN-Department of Control and Computer Engineering, Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Palena","sequence":"additional","affiliation":[{"name":"CNIT-National Inter-University Consortium for Telecommunications, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6233-0994","authenticated-orcid":false,"given":"Paolo","family":"Pasini","sequence":"additional","affiliation":[{"name":"DET-Department of Electronics and Telecommunications, Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","volume-title":"2022 Wilson research group FPGA functional verification trends","author":"Foster","year":"2022"},{"issue":"6","key":"ref2","doi-asserted-by":"crossref","first-page":"253","DOI":"10.3390\/a17060253","article-title":"Hardware model checking algorithms and techniques","volume":"17","author":"Cabodi","year":"2024","journal-title":"Algorithms"},{"issue":"1","key":"ref3","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","article-title":"Bounded model checking using satisfiability solving","volume":"19","author":"Clarke","year":"2001","journal-title":"Formal Methods Syst. Des."},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-022-00406-7"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49519-3_18"},{"issue":"12","key":"ref9","first-page":"1693","article-title":"Improving SAT-based bounded model checking by means of BDD-based approximate traversals","volume":"10","author":"Cabodi","year":"2004","journal-title":"J. Universal Comput. Sci."},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2019.2915317"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_15"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57249-4_8"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"ref14","volume-title":"The Minisat SAT Solver","author":"E\u00e9n","year":"2009"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2808229"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0451-8"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0123-3"},{"key":"ref20","volume-title":"The Model Checking Competition Web Page","author":"Biere","year":"2024"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/6287639\/10380310\/10643065.pdf?arnumber=10643065","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T05:48:49Z","timestamp":1726033729000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10643065\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"references-count":20,"URL":"https:\/\/doi.org\/10.1109\/access.2024.3446802","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]}}}