{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T13:06:41Z","timestamp":1748351201136,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031224751"},{"type":"electronic","value":"9783031224768"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-22476-8_8","type":"book-chapter","created":{"date-parts":[[2022,11,30]],"date-time":"2022-11-30T12:03:51Z","timestamp":1669809831000},"page":"124-142","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Level-Up - From Bits to\u00a0Words"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1002-6023","authenticated-orcid":false,"given":"Matthias","family":"G\u00fcdemann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Riedl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,12,1]]},"reference":[{"key":"8_CR1","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.smt-lib.org\/"},{"key":"8_CR2","unstructured":"Biere, A.: Tutorial on world-level model checking. In: 2020 Formal Methods in Computer Aided Design (FMCAD) (2020)"},{"key":"8_CR3","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). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"8_CR4","unstructured":"Biere, A., Claessen, K.: Hardware model checking competition. In: Hardware Verification Workshop (2010)"},{"key":"8_CR5","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond (2011)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-540-70545-1_43","volume-title":"Computer Aided Verification","author":"P Bjesse","year":"2008","unstructured":"Bjesse, P.: A practical approach to word level model checking of industrial netlists. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 446\u2013458. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_43"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Bjesse, P.: Word-level sequential memory abstraction for model checking. In: 2008 Formal Methods in Computer-Aided Design (2008)","DOI":"10.1109\/FMCAD.2008.ECP.20"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/s10703-009-0080-2","volume":"35","author":"P Bjesse","year":"2009","unstructured":"Bjesse, P.: Word-level bitwidth reduction for unbounded hardware model checking. Formal Methods Syst. Des. 35(1), 56\u201372 (2009). https:\/\/doi.org\/10.1007\/s10703-009-0080-2","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-40922-X_23","volume-title":"Formal Methods in Computer-Aided Design","author":"P Bjesse","year":"2000","unstructured":"Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 409\u2013426. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_23"},{"key":"8_CR10","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":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-319-33951-1_17","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"N Breton","year":"2016","unstructured":"Breton, N., Fonteneau, Y.: S3: proving the safety of critical systems. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds.) RSSRail 2016. LNCS, vol. 9707, pp. 231\u2013242. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33951-1_17"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/978-3-319-41540-6_29","volume-title":"Computer Aided Verification","author":"A Champion","year":"2016","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 510\u2013517. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-31424-7_23","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277\u2013293. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_23"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-96142-2_3","volume-title":"Computer Aided Verification","author":"A Gacek","year":"2018","unstructured":"Gacek, A., Backes, J., Whalen, M., Wagner, L., Ghassabani, E.: The JKind model checker. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 20\u201327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_3"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-030-20652-9_11","volume-title":"NASA Formal Methods","author":"A Goel","year":"2019","unstructured":"Goel, A., Sakallah, K.: Model checking of Verilog RTL using IC3 with syntax-guided abstraction. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 166\u2013185. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_11"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-54862-8_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gurfinkel","year":"2014","unstructured":"Gurfinkel, A., Belov, A., Marques-Silva, J.: Synthesizing safe bit-precise invariants. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 93\u2013108. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_7"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Ivrii, A.: K-induction without unrolling. In: FMCAD (2017)","DOI":"10.23919\/FMCAD.2017.8102253"},{"key":"8_CR18","unstructured":"Jahier, E., Raymond, P., Halbwachs, N.: The lustre V6 reference manual. Verimag, Grenoble (2016)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Dutertre, B.: Property-directed K-induction. In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp. 85\u201392 (2016)","DOI":"10.1109\/FMCAD.2016.7886665"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-34188-5_9","volume-title":"Hardware and Software: Verification and Testing","author":"Z Khasidashvili","year":"2012","unstructured":"Khasidashvili, Z., Nadel, A.: Implicative simultaneous satisfiability and applications. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 66\u201379. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_9"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-030-81688-9_22","volume-title":"Computer Aided Verification","author":"M Mann","year":"2021","unstructured":"Mann, M., et al.: Pono: a flexible and extensible SMT-based model checker. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 461\u2013474. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Mattarei, C., Mann, M., Barrett, C., Daly, R.G., Huff, D., Hanrahan, P.: CoSA: integrated verification for agile hardware design. In: Formal Methods in Computer-Aided Design, FMCAD 2018, Austin, Texas, USA, 30 October\u20132 November 2018. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603014"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-319-96145-3_32","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2018","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC and Boolector\u00a03.0. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 587\u2013595. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_32"},{"key":"8_CR24","unstructured":"Ordioni, J., Breton, N., Cola\u00e7o, J.L.: HLL v. 2.7 modelling language specification (2018)"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127\u2013144. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-49519-3_7","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"1998","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on st\u00e5lmarck\u2019s proof procedure for propositional logic. In: Gopalakrishnan, G., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 82\u201399. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49519-3_7"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Tange, O.: GNU parallel 20220322 (2022). https:\/\/doi.org\/10.5281\/zenodo.6377950","DOI":"10.5281\/zenodo.6377950"},{"key":"8_CR28","unstructured":"Wolf, C., Glaser, J.: Yosys-a free verilog synthesis suite. In: Proceedings of the 21st Austrian Workshop on Microelectronics (Austrochip) (2013)"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-030-67067-2_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Zhang","year":"2021","unstructured":"Zhang, H., Gupta, A., Malik, S.: Syntax-guided synthesis for lemma generation in hardware model checking. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 325\u2013349. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_15"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22476-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,30]],"date-time":"2022-11-30T12:05:09Z","timestamp":1669809909000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22476-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031224751","9783031224768"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22476-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SBMF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazilian Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 December 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sites.google.com\/dcomp.ufs.br\/sbmf2022","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}