{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T06:10:13Z","timestamp":1747894213173,"version":"3.41.0"},"reference-count":40,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["DGE-1656518"],"award-info":[{"award-number":["DGE-1656518"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,3,31]]},"DOI":"10.23919\/date64628.2025.10993135","type":"proceedings-article","created":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T17:36:35Z","timestamp":1747848995000},"page":"1-7","source":"Crossref","is-referenced-by-count":0,"title":["Efficient SAT-Based Bounded Model Checking of Evolving Systems"],"prefix":"10.23919","author":[{"given":"Sophie","family":"Andrews","sequence":"first","affiliation":[{"name":"Stanford University"}]},{"given":"Matthew","family":"Sotoudeh","sequence":"additional","affiliation":[{"name":"Stanford University"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[{"name":"Stanford University"}]}],"member":"263","reference":[{"journal-title":"Riscv-formal","year":"2024","author":"Wolf","key":"ref1"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.3233\/faia200987"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"},{"journal-title":"Aiger 1.9 and beyond","year":"2011","author":"Biere","key":"ref4"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2002.804386"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378470"},{"journal-title":"Yosys open synthesis suite","author":"Wolf","key":"ref7"},{"key":"ref8","first-page":"51","article-title":"CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020","volume-title":"Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, ser. Department of Computer Science Report Series B, T. Balyo, N. Froleyks, M. Heule, M. Iser, M. J\u00e4rvisalo, and M. Suda, Eds.","volume":"B-2020-1","author":"Biere"},{"key":"ref9","article-title":"Efficient sat-based bounded model checking of evolving systems","author":"Andrews","year":"2025","journal-title":"DATE"},{"journal-title":"Hwmcc\u201920","year":"2020","key":"ref10"},{"key":"ref11","article-title":"Incremental formal verification of hardware","author":"Chockler","year":"2011","journal-title":"2011 Formal Methods in Computer-Aided Design, FMCAD 2011"},{"key":"ref12","article-title":"The rocket chip generator","author":"Asanovi\u0107","year":"2016","journal-title":"EECS Department, University of California, Berkeley, Tech. Rep. UCB\/EECS-2016-17"},{"journal-title":"Vexriscv","author":"S. H.","key":"ref13"},{"journal-title":"Nerv","year":"2023","author":"Wolf","key":"ref14"},{"journal-title":"Picorv32","year":"2024","author":"Wolf","key":"ref15"},{"journal-title":"Serv","year":"2024","author":"Kindgren","key":"ref16"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534399"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/icsme.2018.00044"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45234-6_2"},{"volume-title":"Software Abstractions - Logic, Language, and Analysis","year":"2006","author":"Jackson","key":"ref21"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_10"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10623-6_6"},{"key":"ref24","article-title":"Incremental bounded model checking for embedded software (extended version)","volume":"abs\/1409.5872","author":"Schrammel","year":"2014","journal-title":"CoRR"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2000.878311"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379019"},{"article-title":"On incremental satisfiability and bounded model checking","volume-title":"First International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS11)","author":"Wieringa","key":"ref27"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491429"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102255"},{"issue":"02","key":"ref30","doi-asserted-by":"crossref","first-page":"1652","DOI":"10.1609\/aaai.v34i02.5527","article-title":"Hard examples for common variable decision heuristics","volume":"34","author":"Vinyals","journal-title":"Proceedings of the AAAI Conference on Artificial Intelligence"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_24"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-44953-1_30"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_25"},{"key":"ref34","article-title":"On using unsatisfiability for solving maximum satisfiability","volume":"abs\/0712.1097","author":"Marques-Silva","year":"2007","journal-title":"CoRR"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_44"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/1366110.1366131"},{"key":"ref37","article-title":"Graph symmetry detection and canonical labeling: Differences and synergies","volume":"abs\/1208.6271","author":"Katebi","year":"2012","journal-title":"CoRR"},{"journal-title":"Engineering an Efficient Canonical Labeling Tool for Large and Sparse Graphs","first-page":"135","author":"Junttila","key":"ref38"},{"key":"ref39","first-page":"349","article-title":"Acceleration of sat-based iterative property checking","volume-title":"Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbr\u00fccken, Germany, October 3\u20136, 2005, Proceedings, ser. Lecture Notes in Computer Science, D. Borrione and W. J. Paul, Eds.","volume":"3725","author":"Gro\u03b2e"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-929-5-825"}],"event":{"name":"2025 Design, Automation & Test in Europe Conference (DATE)","start":{"date-parts":[[2025,3,31]]},"location":"Lyon, France","end":{"date-parts":[[2025,4,2]]}},"container-title":["2025 Design, Automation & Test in Europe Conference (DATE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/10992638\/10992588\/10993135.pdf?arnumber=10993135","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T05:33:16Z","timestamp":1747891996000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10993135\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,31]]},"references-count":40,"URL":"https:\/\/doi.org\/10.23919\/date64628.2025.10993135","relation":{},"subject":[],"published":{"date-parts":[[2025,3,31]]}}}