{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:34:02Z","timestamp":1767929642094,"version":"3.49.0"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031634970","type":"print"},{"value":"9783031634987","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_17","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"284-303","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Certifying Phase Abstraction"],"prefix":"10.1007","author":[{"given":"Nils","family":"Froleyks","sequence":"first","affiliation":[]},{"given":"Emily","family":"Yu","sequence":"additional","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]},{"given":"Keijo","family":"Heljanko","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/10930755_11","volume-title":"Theorem Proving in Higher Order Logics","author":"H Amjad","year":"2003","unstructured":"Amjad, H.: Programming a symbolic model checker in a fully expansive theorem prover. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 171\u2013187. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/10930755_11"},{"key":"17_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"17_CR3","unstructured":"Balyo, T., Heule, M.J.H.: Proceedings of SAT competition 2016 \u2013 solver and benchmark descriptions. Department of Computer Science Series of Publications B, vol. B-2016-1. University of Helsinki (2016)"},{"issue":"10","key":"17_CR4","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3587692","volume":"66","author":"H Barbosa","year":"2023","unstructured":"Barbosa, H., et al.: Generating and exploiting automated reasoning proof certificates. Commun. ACM 66(10), 86\u201395 (2023). https:\/\/doi.org\/10.1145\/3587692","journal-title":"Commun. ACM"},{"key":"17_CR5","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-031-10769-6_3","volume-title":"IJCAR 2022","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: Flexible proof production in an industrial-strength SMT solver. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 15\u201335. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_3"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-48683-6_9","volume-title":"Computer Aided Verification","author":"J Baumgartner","year":"1999","unstructured":"Baumgartner, J., Heyman, T., Singhal, V., Aziz, A.: Model checking the IBM gigahertz processor: an abstraction algorithm for high-performance netlists. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 72\u201383. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_9"},{"key":"17_CR7","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1023\/A:1024485130001","volume":"23","author":"J Baumgartner","year":"2003","unstructured":"Baumgartner, J., Heyman, T., Singhal, V., Aziz, A.: An abstraction algorithm for the verification of level-sensitive latch-based netlists. Formal Methods Syst. Des. 23, 39\u201365 (2003)","journal-title":"Formal Methods Syst. Des."},{"key":"17_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-031-30820-8_12","volume-title":"TACAS 2023","author":"D Beyer","year":"2023","unstructured":"Beyer, D., Chien, P., Lee, N.: Bridging hardware and software analysis with Btor2C: a word-level-circuit-to-C translator. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 152\u2013172. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_12"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: SIGSOFT FSE, pp. 326\u2013337. ACM (2016)","DOI":"10.1145\/2950290.2950351"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Lemberger, T., Tautschnig, M.: Verification witnesses. ACM Trans. Softw. Eng. Methodol. 31(4), 57:1\u201357:69 (2022)","DOI":"10.1145\/3477579"},{"key":"17_CR11","doi-asserted-by":"publisher","unstructured":"Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 739\u2013764. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201002","DOI":"10.3233\/FAIA201002"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Biere, A., Brummayer, R.: Consistency checking of all different constraints over bit-vectors within a SAT solver. In: FMCAD, pp.\u00a01\u20134. IEEE (2008)","DOI":"10.1109\/FMCAD.2008.ECP.32"},{"key":"17_CR13","unstructured":"Biere, A., Claessen, K.: Hardware model checking competition 2010 (2010). http:\/\/fmv.jku.at\/hwmcc10\/"},{"key":"17_CR14","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical report, FMV Reports Series, Inst. FMV, JKU Linz, Austria (2011)"},{"key":"17_CR15","unstructured":"Biere, A., Yu, E., Froleyks, N.: Stratified certification for k-induction. In: FMCAD, vol.\u00a03, p.\u00a059. TU Wien Academic Press (2022)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Kukula, J.H.: Automatic generalized phase abstraction for formal verification. In: ICCAD, pp. 1076\u20131082. IEEE Computer Society (2005)","DOI":"10.1109\/ICCAD.2005.1560220"},{"key":"17_CR17","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":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"17_CR19","unstructured":"Case, M.L., Baumgartner, J., Mony, H., Kanzelman, R.: Approximate reachability with combined symbolic and ternary simulation. In: FMCAD, pp. 109\u2013115. FMCAD Inc. (2011)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Case, M.L., Mony, H., Baumgartner, J., Kanzelman, R.: Enhanced verification by temporal decomposition. In: FMCAD, pp. 17\u201324. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351146"},{"key":"17_CR21","unstructured":"Certifaiger: Certifaiger (2021). http:\/\/fmv.jku.at\/certifaiger"},{"key":"17_CR22","volume-title":"Model Checking","author":"EM Clarke","year":"2018","unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model Checking, 2nd edn. MIT Press, Cambridge (2018)","edition":"2"},{"key":"17_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 611\u2013706. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50012-6"},{"key":"17_CR25","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: FMCAD, pp. 125\u2013134. FMCAD Inc. (2011)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"van Eijk, C.A.J., Jess, J.A.G.: Exploiting functional dependencies in finite state machine verification. In: ED &TC, pp. 9\u201314. IEEE Computer Society (1996)","DOI":"10.1109\/EDTC.1996.494119"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 463\u2013478. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_31"},{"key":"17_CR28","unstructured":"Fleury, M., Biere, A.: Mining definitions in Kissat with Kittens. Formal Methods Syst. Des. 1\u201324 (2023)"},{"key":"17_CR29","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2021.103572","volume":"301","author":"N Froleyks","year":"2021","unstructured":"Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M.: Sat competition 2020. Artif. Intell. 301, 103572 (2021)","journal-title":"Artif. Intell."},{"issue":"11","key":"17_CR30","doi-asserted-by":"publisher","first-page":"2052","DOI":"10.1109\/JPROC.2015.2476472","volume":"103","author":"M Fujita","year":"2015","unstructured":"Fujita, M.: Toward unification of synthesis and verification in topologically constrained logic design. Proc. IEEE 103(11), 2052\u20132060 (2015)","journal-title":"Proc. IEEE"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for LTL model checking. In: FMCAD, pp.\u00a01\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603022"},{"issue":"2","key":"17_CR32","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/s10703-021-00369-1","volume":"57","author":"A Griggio","year":"2021","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for SAT-based model checking. Formal Methods Syst. Des. 57(2), 178\u2013210 (2021)","journal-title":"Formal Methods Syst. Des."},{"key":"17_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-66107-0_18","volume-title":"Interactive Theorem Proving","author":"M Heule","year":"2017","unstructured":"Heule, M., Hunt, W., Kaufmann, M., Wetzler, N.: Efficient, verified checking of propositional proofs. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 269\u2013284. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_18"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Heule, M.J.: Proofs of unsatisfiability. In: Handbook of Satisfiability, pp. 635\u2013668. IOS Press (2021)","DOI":"10.3233\/FAIA200998"},{"key":"17_CR35","unstructured":"Heule, M.J., Biere, A.: Proofs for satisfiability problems. In: All About Proofs, Proofs for All, vol. 55, no. 1, pp. 1\u201322 (2015)"},{"key":"17_CR36","unstructured":"Hoenicke, J., Schindler, T.: A simple proof format for SMT. In: D\u00e9harbe, D., Hyv\u00e4rinen, A.E.J. (eds.) Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, 11\u201312 August 2022. CEUR Workshop Proceedings, vol.\u00a03185, pp. 54\u201370. CEUR-WS.org (2022)"},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Kaufmann, D., Fleury, M., Biere, A., Kauers, M.: Practical algebraic calculus and nullstellensatz with the checkers pacheck and past\u00e8que and nuss-checker. Formal Methods Syst. Des. 1\u201335 (2022)","DOI":"10.1007\/s10703-022-00391-x"},{"key":"17_CR38","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 21(12), 1377\u20131394 (2002)","DOI":"10.1109\/TCAD.2002.804386"},{"key":"17_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-319-03077-7_3","volume-title":"Hardware and Software: Verification and Testing","author":"T Kuismin","year":"2013","unstructured":"Kuismin, T., Heljanko, K.: Increasing confidence in liveness model checking results with proofs. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 32\u201343. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03077-7_3"},{"key":"17_CR40","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2019.103229","volume":"281","author":"JM Lagniez","year":"2020","unstructured":"Lagniez, J.M., Lonca, E., Marquis, P.: Definability for model counting. Artif. Intell. 281, 103229 (2020)","journal-title":"Artif. Intell."},{"issue":"3","key":"17_CR41","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s10817-019-09525-z","volume":"64","author":"P Lammich","year":"2020","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reason. 64(3), 513\u2013532 (2020)","journal-title":"J. Autom. Reason."},{"key":"17_CR42","doi-asserted-by":"crossref","unstructured":"Mebsout, A., Tinelli, C.: Proof certificates for SMT-based model checkers for infinite-state systems. In: FMCAD, pp. 117\u2013124. IEEE (2016)","DOI":"10.1109\/FMCAD.2016.7886669"},{"key":"17_CR43","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K.: Dag-aware AIG rewriting a fresh look at combinational logic synthesis. In: DAC, pp. 532\u2013535. ACM (2006)","DOI":"10.1145\/1146909.1147048"},{"key":"17_CR44","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K., E\u00e9n, N.: Improvements to combinational equivalence checking. In: ICCAD, pp. 836\u2013843. ACM (2006)","DOI":"10.1109\/ICCAD.2006.320087"},{"key":"17_CR45","unstructured":"Mishchenko, A., Chatterjee, S., Jiang, R., Brayton, R.K.: FRAIGs: a unifying representation for logic synthesis and verification. Technical report, ERL Technical Report (2005)"},{"key":"17_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/11560548_21","volume-title":"Correct Hardware Design and Verification Methods","author":"H Mony","year":"2005","unstructured":"Mony, H., Baumgartner, J., Aziz, A.: Exploiting constraints in transformation-based verification. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 269\u2013284. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11560548_21"},{"key":"17_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-44585-4_2","volume-title":"Computer Aided Verification","author":"KS Namjoshi","year":"2001","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2\u201313. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_2"},{"key":"17_CR48","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"17_CR49","doi-asserted-by":"crossref","unstructured":"Padoa, A.: Essai d\u2019une th\u00e9orie alg\u00e9brique des nombres entiers, pr\u00e9c\u00e9d\u00e9 d\u2019une introduction logique \u00e0 une theorie d\u00e9ductive quelconque. In: Biblioth\u00e8que du Congr\u00e8s international de philosophie, vol.\u00a03, pp. 309\u2013365 (1901)","DOI":"10.5840\/wcp11901312"},{"key":"17_CR50","unstructured":"Paulson, L., Nipkow, T.: The sledgehammer: let automatic theorem provers write your isabelle scripts (2023)"},{"key":"17_CR51","doi-asserted-by":"publisher","unstructured":"Schurr, H., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: towards a generic SMT proof format (extended abstract). In: Keller, C., Fleury, M. (eds.) Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, 11 July 2021. EPTCS, vol.\u00a0336, pp. 49\u201354 (2021). https:\/\/doi.org\/10.4204\/EPTCS.336.6","DOI":"10.4204\/EPTCS.336.6"},{"issue":"2","key":"17_CR52","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"CH Seger","year":"1995","unstructured":"Seger, C.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods Syst. Des. 6(2), 147\u2013189 (1995)","journal-title":"Formal Methods Syst. Des."},{"key":"17_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/978-3-030-53288-8_24","volume-title":"Computer Aided Verification","author":"F Slivovsky","year":"2020","unstructured":"Slivovsky, F.: Interpolation-based semantic gate extraction and its applications to QBF preprocessing. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 508\u2013528. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_24"},{"key":"17_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0054171","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Sprenger","year":"1998","unstructured":"Sprenger, C.: A verified model checker for the modal $$\\mu $$-calculus in Coq. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 167\u2013183. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054171"},{"key":"17_CR55","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970, pp. 466\u2013483 (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"17_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-030-81688-9_17","volume-title":"Computer Aided Verification","author":"E Yu","year":"2021","unstructured":"Yu, E., Biere, A., Heljanko, K.: Progress in certifying hardware model checking results. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 363\u2013386. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_17"},{"key":"17_CR57","unstructured":"Yu, E., Froleyks, N., Biere, A., Heljanko, K.: Towards compositional hardware model checking certification. In: FMCAD (2023)"},{"key":"17_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/11499107_42","volume-title":"Theory and Applications of Satisfiability Testing","author":"L Zhang","year":"2005","unstructured":"Zhang, L.: On subsumption removal and on-the-fly CNF simplification. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 482\u2013489. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11499107_42"},{"key":"17_CR59","doi-asserted-by":"crossref","unstructured":"Zhu, Q., Kitchen, N., Kuehlmann, A., Sangiovanni-Vincentelli, A.L.: SAT sweeping with local observability don\u2019t-cares. In: DAC, pp. 229\u2013234. ACM (2006)","DOI":"10.1145\/1146909.1146970"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:28Z","timestamp":1747592248000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}