{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T10:50:30Z","timestamp":1742986230621,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030451899"},{"type":"electronic","value":"9783030451905"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45190-5_20","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T09:03:02Z","timestamp":1587114182000},"page":"367-386","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Partial Order Reduction for Deep Bug Finding in Synchronous Hardware"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1555-5784","authenticated-orcid":false,"given":"Makai","family":"Mann","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"20_CR1","unstructured":"Bailey, B.: When bugs escape (July 2018), \nhttps:\/\/semiengineering.com\/when-bugs-escape\/\n\n, [Online]"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de\u00a0Simone, R. (eds.) CONCUR\u201998 Concurrency Theory. pp. 485\u2013500. Springer Berlin Heidelberg, Berlin, Heidelberg (1998)","DOI":"10.1007\/BFb0055643"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Bhattacharya, R., German, S., Gopalakrishnan, G.: Symbolic partial order reduction for rule based transition systems. In: Borrione, D., Paul, W. (eds.) Correct Hardware Design and Verification Methods, pp. 332\u2013335. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)","DOI":"10.1007\/11560548_25"},{"key":"20_CR4","unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2017. In: Balyo, T., Heule, M., J\u00e4rvisalo, M. (eds.) Proc. of SAT Competition 2017 - Solver and Benchmark Descriptions. vol. B-2017-1, pp. 14\u201315. University of Helsinki (2017)"},{"issue":"2","key":"20_CR5","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","volume":"66","author":"A Biere","year":"2002","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electr. Notes Theor. Comput. Sci. 66(2), 160\u2013177 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 193\u2013207. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"20_CR7","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. rep., FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Bjesse, P.: A practical approach to word level model checking of industrial netlists. pp. 446\u2013458 (07 2008)","DOI":"10.1007\/978-3-540-70545-1_43"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Bjesse, P.: Word-level sequential memory abstraction for model checking. In: FMCAD. pp. 1\u20139. IEEE (2008)","DOI":"10.1109\/FMCAD.2008.ECP.20"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: Sat-based model checking without unrolling. In: VMCAI. Lecture Notes in Computer Science, vol.\u00a06538, pp. 70\u201387. Springer (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Brayton, R., Mishchenko, A.: Abc: An academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification, pp. 24\u201340. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"20_CR12","doi-asserted-by":"publisher","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2) (1992). \nhttps:\/\/doi.org\/10.1016\/0890-5401(92)90017-A","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions inmodel checking. In: CAV. Lecture Notes in Computer Science, vol. 1427, pp. 147\u2013158. Springer (1998)","DOI":"10.1007\/BFb0028741"},{"key":"20_CR14","unstructured":"Clarke, Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge, MA, USA (1999)"},{"key":"20_CR15","unstructured":"Clarke, E., Henzinger, T., Veith, H.: Handbook of Model Checking. Springer International Publishing (2016), \nhttps:\/\/books.google.com\/books?id=qxG8oAEACAAJ"},{"key":"20_CR16","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: FMCAD. pp. 125\u2013134. FMCAD Inc. (2011)"},{"issue":"1","key":"20_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/1000000013","volume":"3","author":"H Foster","year":"2009","unstructured":"Foster, H.: Applied assertion-based verification: An industry perspective. Foundations and Trends in Electronic Design Automation 3(1), 1\u201395 (2009)","journal-title":"Foundations and Trends in Electronic Design Automation"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Gupta, A.: Accelerating high-level bounded model checking. In: ICCAD. pp. 794\u2013801. ACM (2006)","DOI":"10.1109\/ICCAD.2006.320122"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Gupta, A., Ganai, M.K., Wang, C., Yang, Z., Ashar, P.: Learning from bdds in sat-based bounded model checking. In: DAC. pp. 824\u2013829. ACM (2003)","DOI":"10.1145\/775832.776040"},{"key":"20_CR20","unstructured":"Johannsen, P.: Speeding Up Hardware Verification by Automated Data Path Scaling. Ph.D. thesis, University of Kiel (2002)"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In: CAV. Lecture Notes in Computer Science, vol.\u00a05643, pp. 398\u2013413. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_31"},{"key":"20_CR22","unstructured":"Kocher, P., Genkin, D., Gruss, D., Haas, W., Hamburg, M., Lipp, M., Mangard, S., Prescher, T., Schwarz, M., Yarom, Y.: Spectre attacks: Exploiting speculative execution. CoRR abs\/1801.01203 (2018), \nhttp:\/\/arxiv.org\/abs\/1801.01203"},{"key":"20_CR23","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer Publishing Company, Incorporated (2008)"},{"key":"20_CR24","volume-title":"Hardware Design Verification: Simulation and Formal Method-Based Approaches (Prentice Hall Modern Semiconductor Design Series)","author":"WK Lam","year":"2005","unstructured":"Lam, W.K.: Hardware Design Verification: Simulation and Formal Method-Based Approaches (Prentice Hall Modern Semiconductor Design Series). Prentice Hall PTR, Upper Saddle River, NJ, USA (2005)"},{"key":"20_CR25","unstructured":"Lipp, M., Schwarz, M., Gruss, D., Prescher, T., Haas, W., Mangard, S., Kocher, P., Genkin, D., Yarom, Y., Hamburg, M.: Meltdown. CoRR abs\/1801.01207 (2018)"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Mattarei, C., Mann, M., Barrett, C.W., Daly, R.G., Huff, D., Hanrahan, P.: Cosa: Integrated verification for agile hardware design. In: FMCAD. pp. 1\u20135. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603014"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and sat-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) Computer Aided Verification, pp. 1\u201313. Springer Berlin Heidelberg, Berlin, Heidelberg (2003)","DOI":"10.1007\/978-3-540-45069-6_1"},{"issue":"1\u20133","key":"20_CR28","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0167-6423(99)00030-1","volume":"37","author":"KL McMillan","year":"2000","unstructured":"McMillan, K.L.: A methodology for hardware verification using compositional model checking. Sci. Comput. Program. 37(1\u20133), 279\u2013309 (2000)","journal-title":"Sci. Comput. Program."},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, btormc and boolector 3.0. In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 587\u2013595. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Peled, D.: Verification for robust specification. In: Gunter, E.L., Felty, A. (eds.) Theorem Proving in Higher Order Logics. pp. 231\u2013241. Springer Berlin Heidelberg, Berlin, Heidelberg (1997)","DOI":"10.1007\/BFb0028397"},{"issue":"2","key":"20_CR31","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S0304-3975(97)00219-3","volume":"195","author":"DA Peled","year":"1998","unstructured":"Peled, D.A., Wilke, T., Wolper, P.: An algorithmic approach for checking closure properties of temporal logic specifications and omega-regular languages. Theor. Comput. Sci. 195(2), 183\u2013203 (1998)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"20_CR32","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1109\/40.372360","volume":"15","author":"D Price","year":"1995","unstructured":"Price, D.: Pentium fdiv flaw-lessons learned. IEEE Micro 15(2), 86\u201388 (1995). \nhttps:\/\/doi.org\/10.1109\/40.372360","journal-title":"IEEE Micro"},{"key":"20_CR33","doi-asserted-by":"publisher","unstructured":"Sagstetter, F., Lukasiewycz, M., Steinhorst, S., Wolf, M., Bouard, A., R. Harris, W., Jha, S., Peyrin, T., Poschmann, A., Chakraborty, S.: Security challenges in automotive hardware\/software architecture design. pp. 458\u2013463 (01 2013). \nhttps:\/\/doi.org\/10.7873\/DATE.2013.102","DOI":"10.7873\/DATE.2013.102"},{"issue":"6","key":"20_CR34","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1109\/MM.2010.81","volume":"30","author":"O Shacham","year":"2010","unstructured":"Shacham, O., Azizi, O., Wachs, M., Richardson, S., Horowitz, M.: Rethinking digital design: Why design must change. IEEE Micro 30(6), 9\u201324 (2010)","journal-title":"IEEE Micro"},{"key":"20_CR35","doi-asserted-by":"crossref","unstructured":"Strichman, O.: Tuning SAT checkers for bounded model checking. In: CAV. Lecture Notes in Computer Science, vol.\u00a01855, pp. 480\u2013494. Springer (2000)","DOI":"10.1007\/10722167_36"},{"issue":"1","key":"20_CR36","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/B:FORM.0000004785.67232.f8","volume":"24","author":"O Strichman","year":"2004","unstructured":"Strichman, O.: Accelerating bounded model checking of safety properties. Formal Methods in System Design 24(1), 5\u201324 (2004)","journal-title":"Formal Methods in System Design"},{"key":"20_CR37","doi-asserted-by":"crossref","unstructured":"Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 382\u2013396. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_29"},{"key":"20_CR38","unstructured":"Wolf, C., Glaser, J., Kepler, J.: Yosys-a free Verilog synthesis suite. In: Proceedings of the 21st Austrian Workshop on Microelectronics (Austrochip) (2013)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45190-5_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,20]],"date-time":"2020-08-20T13:11:29Z","timestamp":1597929089000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45190-5_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030451899","9783030451905"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45190-5_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","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":"155","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":"40","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":"8","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":"26% - 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":"14","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)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}