{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:34Z","timestamp":1784793814900,"version":"3.55.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Formal hardware verification ensures that a design satisfies its specifications, but writing these specifications requires substantial manual effort. Specification mining automates this process, and existing work has their own merits. The classic approaches rely on pre-defined templates, which have limited expressiveness and lack formal correctness guarantees. However, recent years have seen the emergence of using formal program synthesis for specification mining, which provides general and correct specifications but struggles to scale to complex designs.<\/jats:p>\n                  <jats:p>In this work, we present MAPminer, a parallel framework for synthesis-based hardware specification mining. MAPminer exploits its novel algorithm based on the Maximal Universal Subset and partitions the synthesis problem into efficient sub-problems. These sub-problems are automatically scheduled across multiple threads for parallel synthesis. Experimental results show that MAPminer produces more effective assertions, improving verification coverage while reducing assertion size.<\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_21","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:24Z","timestamp":1784791044000},"page":"403-425","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Massively Parallel Mining of Specifications for\u00a0Hardware Designs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-6026-4632","authenticated-orcid":false,"given":"Leiqi","family":"Ye","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5809-3455","authenticated-orcid":false,"given":"Guy","family":"Frankel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2791-2555","authenticated-orcid":false,"given":"Jianyi","family":"Cheng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9032-7661","authenticated-orcid":false,"given":"Elizabeth","family":"Polgreen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"21_CR1","unstructured":"EBMC. https:\/\/github.com\/diffblue\/hw-cbmc\/"},{"key":"21_CR2","unstructured":"Circuit netlist benchmarks (2025). https:\/\/sportlab.usc.edu\/~msabrishami\/benchmarks.html"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-319-09284-3_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"G Audemard","year":"2014","unstructured":"Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197\u2013205. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_15"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-319-24318-4_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"T Balyo","year":"2015","unstructured":"Balyo, T., Sanders, P., Sinz, C.: HordeSat: a massively parallel portfolio SAT solver. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 156\u2013172. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_12"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"21_CR6","first-page":"1","volume":"2013","author":"A Biere","year":"2013","unstructured":"Biere, A., et al.: Lingeling, Plingeling and Treengeling entering the SAT competition 2013. Proc. SAT Compet. 2013, 1 (2013)","journal-title":"Proc. SAT Compet."},{"issue":"1","key":"21_CR7","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001). https:\/\/doi.org\/10.1023\/A:1011276507260","journal-title":"Formal Methods Syst. Des."},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-642-31424-7_30","volume-title":"Computer Aided Verification","author":"I Dillig","year":"2012","unstructured":"Dillig, I., Dillig, T., McMillan, K.L., Aiken, A.: Minimum satisfying assignments for SMT. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 394\u2013409. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_30"},{"key":"21_CR9","doi-asserted-by":"publisher","unstructured":"Dinesh, S., Zhu, Y., Fletcher, C.W.: H-Houdini: scalable invariant learning. In: Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1, pp. 603\u2013618 (2025). https:\/\/doi.org\/10.1145\/3669940.3707263","DOI":"10.1145\/3669940.3707263"},{"issue":"1\u20133","key":"21_CR10","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., et al.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007). https:\/\/doi.org\/10.1016\/j.scico.2007.01.015","journal-title":"Sci. Comput. Program."},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-89960-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Fedyukovich","year":"2018","unstructured":"Fedyukovich, G., Bod\u00edk, R.: Accelerating syntax-guided invariant synthesis. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 251\u2013269. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_14"},{"issue":"11","key":"21_CR12","doi-asserted-by":"publisher","first-page":"4277","DOI":"10.1109\/TCAD.2022.3197525","volume":"41","author":"S Germiniani","year":"2022","unstructured":"Germiniani, S., Pravadelli, G.: Harm: a hint-based assertion miner. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), 4277\u20134288 (2022). https:\/\/doi.org\/10.1109\/TCAD.2022.3197525","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Godbole, A., Ye, L., Manerkar, Y.A., Seshia, S.A.: Modelling and verification of security-oriented resource partitioning schemes. In: FMCAD, pp. 268\u2013273 (2023). https:\/\/doi.org\/10.34727\/2023\/isbn.978-3-85448-060-0_35","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_35"},{"issue":"6","key":"21_CR14","doi-asserted-by":"publisher","first-page":"952","DOI":"10.1109\/TCAD.2013.2241176","volume":"32","author":"S Hertz","year":"2013","unstructured":"Hertz, S., Sheridan, D., Vasudevan, S.: Mining hardware assertions with guidance from static analysis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 32(6), 952\u2013965 (2013). https:\/\/doi.org\/10.1109\/TCAD.2013.2241176","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"MJH Heule","year":"2012","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50\u201365. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_8"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-16242-8_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"AEJ Hyv\u00e4rinen","year":"2010","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Partitioning SAT instances for distributed solving. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 372\u2013386. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_27"},{"key":"21_CR18","doi-asserted-by":"publisher","unstructured":"IEEE: Combining dynamic slicing and mutation operators for ESL correction (2012). https:\/\/doi.org\/10.1109\/ETS.2012.6233020","DOI":"10.1109\/ETS.2012.6233020"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-319-44953-1_19","volume-title":"Principles and Practice of Constraint Programming","author":"A Ignatiev","year":"2016","unstructured":"Ignatiev, A., Previti, A., Marques-Silva, J.: On finding minimum satisfying assignments. In: Rueher, M. (ed.) CP 2016. LNCS, vol. 9892, pp. 287\u2013297. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-44953-1_19"},{"key":"21_CR20","doi-asserted-by":"publisher","unstructured":"Iman, M.R.H., Jervan, G., Ghasempouri, T.: Artmine: automatic association rule mining with temporal behavior for hardware verification. In: 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1\u20136. IEEE (2024). https:\/\/doi.org\/10.23919\/DATE58400.2024.10546742","DOI":"10.23919\/DATE58400.2024.10546742"},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Inverso, O., Trubiani, C.: Parallel and distributed bounded model checking of multi-threaded programs. In: Proceedings of the 25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 202\u2013216 (2020). https:\/\/doi.org\/10.1145\/3332466.3374529","DOI":"10.1145\/3332466.3374529"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-319-21668-3_22","volume-title":"Computer Aided Verification","author":"J Jeon","year":"2015","unstructured":"Jeon, J., Qiu, X., Solar-Lezama, A., Foster, J.S.: Adaptive concretization for parallel program synthesis. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 377\u2013394. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_22"},{"issue":"7","key":"21_CR23","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/s00236-017-0294-5","volume":"54","author":"S Jha","year":"2017","unstructured":"Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. Acta Inf. 54(7), 693\u2013726 (2017). https:\/\/doi.org\/10.1007\/s00236-017-0294-5","journal-title":"Acta Inf."},{"key":"21_CR24","doi-asserted-by":"publisher","unstructured":"Kande, R., et al.: LLM-assisted generation of hardware assertions. arXiv preprint arXiv:2306.14027 (2023). https:\/\/doi.org\/10.48550\/arXiv.2306.14027","DOI":"10.48550\/arXiv.2306.14027"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-66263-3_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"S Nejati","year":"2017","unstructured":"Nejati, S., et al.: A propagation rate based splitting heuristic for divide-and-conquer solvers. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 251\u2013260. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_16"},{"key":"21_CR27","doi-asserted-by":"publisher","unstructured":"Orenes-Vera, M., Martonosi, M., Wentzlaff, D.: Using LLMs to facilitate formal verification of RTL. arXiv preprint arXiv:2309.09437 (2023). https:\/\/doi.org\/10.48550\/arXiv.2309.09437","DOI":"10.48550\/arXiv.2309.09437"},{"key":"21_CR28","unstructured":"Raveendran, R., Bhuinya, S.: Customization of ibex RISC-V processor core. Customization of Ibex RISC-V Processor Core (2021)"},{"key":"21_CR29","unstructured":"Rosser, B.J.: Cocotb: a python-based digital logic verification framework. In: Micro-Electronics Section Seminar. CERN, Geneva, Switzerland (2018)"},{"key":"21_CR30","doi-asserted-by":"publisher","first-page":"1437","DOI":"10.1613\/jair.1.15827","volume":"80","author":"D Schreiber","year":"2024","unstructured":"Schreiber, D., Sanders, P.: MallobSat: scalable SAT solving by clause sharing. J. Artif. Intell. Res. 80, 1437\u20131495 (2024). https:\/\/doi.org\/10.1613\/jair.1.15827","journal-title":"J. Artif. Intell. Res."},{"key":"21_CR31","unstructured":"Sun, C., Hahn, C., Trippel, C.: Towards improving verification productivity with circuit-aware translation of natural language to systemverilog assertions. In: First International Workshop on Deep Learning-aided Verification (2023)"},{"key":"21_CR32","doi-asserted-by":"publisher","unstructured":"Yan, Z., et al.: AssertLLM: generating hardware verification assertions from design specifications via multi-LLMs. In: Proceedings of the 30th Asia and South Pacific Design Automation Conference, ASPDAC 2025, pp. 614\u2013621. Association for Computing Machinery, New York, NY, USA (2025). https:\/\/doi.org\/10.1145\/3658617.3697756","DOI":"10.1145\/3658617.3697756"},{"key":"21_CR33","doi-asserted-by":"publisher","unstructured":"Ye, L., Li, Y., Frankel, G., Cheng, J., Polgreen, E.: Unlocking hardware verification with oracle guided synthesis. In: Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, pp. 235\u2013245. TU Wien Academic Press (2025). https:\/\/doi.org\/10.34727\/2025\/isbn.978-3-85448-084-6_30","DOI":"10.34727\/2025\/isbn.978-3-85448-084-6_30"},{"key":"21_CR34","doi-asserted-by":"publisher","unstructured":"Zhao, M., Cai, S., Qian, Y.: Distributed SMT solving based on dynamic variable-level partitioning. In: Computer Aided Verification \u2013 36th International Conference, CAV 2024, Montreal, QC, Canada, 24\u201327 July 2024, Proceedings, Part I, pp. 68\u201388. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_4","DOI":"10.1007\/978-3-031-65627-9_4"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:26Z","timestamp":1784791046000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to\u00a0the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}