{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:00Z","timestamp":1776333480967,"version":"3.51.2"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377082","type":"print"},{"value":"9783031377099","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We apply and evaluate polynomial-time algorithms to compute two different normal forms of propositional formulas arising in verification. One of the normal form algorithms is presented for the first time. The algorithms compute normal forms and solve the word problem for two different subtheories of Boolean algebra: orthocomplemented bisemilattice (OCBSL) and ortholattice (OL). Equality of normal forms decides the word problem and is a sufficient (but not necessary) check for equivalence of propositional formulas. Our first contribution is a quadratic-time OL normal form algorithm, which induces a coarser equivalence than the OCBSL normal form and is thus a more precise approximation of propositional equivalence. The algorithm is efficient even when the input formula is represented as a directed acyclic graph. Our second contribution is the evaluation of OCBSL and OL normal forms as part of a verification condition cache of the Stainless verifier for Scala. The results show that both normalization algorithms substantially increase the cache hit ratio and improve the ability to prove verification conditions by simplification alone. To gain further insights, we also compare the algorithms on hardware circuit benchmarks, showing that normalization reduces circuit size and works well in the presence of sharing.<\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_19","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"398-422","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Formula Normalizations in\u00a0Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8179-7549","authenticated-orcid":false,"given":"Simon","family":"Guilloud","sequence":"first","affiliation":[]},{"given":"Mario","family":"Bucev","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0003-0795-881X","authenticated-orcid":false,"given":"Dragana","family":"Milovan\u010devi\u0107","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7044-9522","authenticated-orcid":false,"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"19_CR1","unstructured":"Amar\u00f9, L., Gaillardon, P.E., De Micheli, G.: The EPFL combinational benchmark suite. In: Proceedings of the 24th International Workshop on Logic & Synthesis (IWLS) (2015). https:\/\/github.com\/lsils\/benchmarks"},{"key":"19_CR2","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: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"19_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-5215-7","volume-title":"Orthomodular Lattices (An Algebraic Approach)","author":"L Beran","year":"1985","unstructured":"Beran, L.: Orthomodular Lattices (An Algebraic Approach). Springer, Dordrecht (1985). https:\/\/doi.org\/10.1007\/978-94-009-5215-7"},{"key":"19_CR4","unstructured":"Birkhoff, G.: Lattice Theory, AMS Colloquium Publications, 3rd edn., vol. 25. AMS (1973)"},{"key":"19_CR5","doi-asserted-by":"publisher","first-page":"3740","DOI":"10.1007\/s10773-016-3258-6","volume":"56","author":"S Bonzio","year":"2017","unstructured":"Bonzio, S., Chajda, I.: A note on orthomodular lattices. Int. J. Theor. Phys. 56, 3740\u20133743 (2017). https:\/\/doi.org\/10.1007\/s10773-016-3258-6","journal-title":"Int. J. Theor. Phys."},{"key":"19_CR6","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"},{"issue":"5","key":"19_CR7","doi-asserted-by":"publisher","first-page":"977","DOI":"10.4153\/CJM-1976-095-6","volume":"28","author":"G Bruns","year":"1976","unstructured":"Bruns, G.: Free ortholattices. Can. J. Math. 28(5), 977\u2013985 (1976). https:\/\/doi.org\/10.4153\/CJM-1976-095-6","journal-title":"Can. J. Math."},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-12002-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150\u2013153. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_12"},{"key":"19_CR9","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-319-10575-8_7","volume-title":"Handbook of Model Checking","author":"RE Bryant","year":"2018","unstructured":"Bryant, R.E.: Binary decision diagrams. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 191\u2013217. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_7"},{"key":"19_CR10","unstructured":"Bucev, M., Kun\u010dak, V.: Formally verified quite OK image format. In: Formal Methods in Computer-Aided Design (FMCAD) (2022)"},{"key":"19_CR11","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979, pp. 269\u2013282. ACM Press (1979). https:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/11916277_33","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"N Dershowitz","year":"2006","unstructured":"Dershowitz, N., Hsiang, J., Huang, G.-S., Kaiss, D.: Boolean rings for intersection-based satisfiability. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 482\u2013496. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11916277_33"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-030-51054-1_24","volume-title":"Automated Reasoning","author":"A Duarte","year":"2020","unstructured":"Duarte, A., Korovin, K.: Implementing superposition in iProver (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 388\u2013397. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_24"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-030-03592-1_4","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"K Even-Mendoza","year":"2018","unstructured":"Even-Mendoza, K., Asadi, S., Hyv\u00e4rinen, A.E.J., Chockler, H., Sharygina, N.: Lattice-based refinement in bounded model checking. In: Piskac, R., R\u00fcmmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 50\u201368. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_4"},{"key":"19_CR15","doi-asserted-by":"publisher","unstructured":"Freese, R., Jezek, J., Nation, J.: Free Lattices, Mathematical Surveys and Monographs, vol. 42. American Mathematical Society, Providence (1995). https:\/\/doi.org\/10.1090\/surv\/042","DOI":"10.1090\/surv\/042"},{"issue":"3","key":"19_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1006\/jsco.1993.1046","volume":"16","author":"R Freese","year":"1993","unstructured":"Freese, R., Jezek, J., Nation, J.B.: Term rewrite systems for lattice theory. J. Symb. Comput. 16(3), 279\u2013288 (1993). https:\/\/doi.org\/10.1006\/jsco.1993.1046","journal-title":"J. Symb. Comput."},{"issue":"2","key":"19_CR17","doi-asserted-by":"publisher","first-page":"174","DOI":"10.2307\/2042634","volume":"77","author":"R Freese","year":"1979","unstructured":"Freese, R., Nation, J.B.: Finitely presented lattices. Proc. Am. Math. Soc. 77(2), 174\u2013178 (1979). https:\/\/doi.org\/10.2307\/2042634","journal-title":"Proc. Am. Math. Soc."},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-642-39274-0_13","volume-title":"Implementation and Application of Automata","author":"T Genet","year":"2013","unstructured":"Genet, T., Le Gall, T., Legay, A., Murat, V.: A completion algorithm for lattice tree automata. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol. 7982, pp. 134\u2013145. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39274-0_13"},{"key":"19_CR19","doi-asserted-by":"publisher","unstructured":"Girard, J.Y.: Une extension de L\u2019interpretation de G\u00f6del a L\u2019analyse, et son application a L\u2019elimination des coupures dans L\u2019analyse et la theorie des types. In: Fenstad, J. (ed.) Proceedings of the Second Scandinavian Logic Symposium, Studies in Logic and the Foundations of Mathematics, vol. 63, pp. 63\u201392. Elsevier (1971). https:\/\/doi.org\/10.1016\/S0049-237X(08)70843-7","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-030-99527-0_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Guilloud","year":"2022","unstructured":"Guilloud, S., Kun\u010dak, V.: Equivalence checking for orthocomplemented bisemilattices in log-linear time. In: TACAS 2022. LNCS, vol. 13244, pp. 196\u2013214. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_11"},{"key":"19_CR21","doi-asserted-by":"publisher","unstructured":"Hamza, J., Felix, S., Kun\u010dak, V., Nussbaumer, I., Schramka, F.: From verified Scala to STIX file system embedded code using Stainless. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, vol. 13260, pp. 393\u2013410. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_21. http:\/\/infoscience.epfl.ch\/record\/292424","DOI":"10.1007\/978-3-031-06773-0_21"},{"key":"19_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3360592","volume":"3","author":"J Hamza","year":"2019","unstructured":"Hamza, J., Voirol, N., Kun\u010dak, V.: System FR: formalized foundations for the Stainless verifier. Proc. ACM Program. Lang. 3, 1\u201330 (2019). https:\/\/doi.org\/10.1145\/3360592","journal-title":"Proc. ACM Program. Lang."},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60\u201366. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/11814948_10","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"H Jain","year":"2006","unstructured":"Jain, H., Bartzis, C., Clarke, E.: Satisfiability checking of non-clausal formulas using general matings. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 75\u201389. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_10"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02777-2_5","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"A Kojevnikov","year":"2009","unstructured":"Kojevnikov, A., Kulikov, A.S., Yaroslavtsev, G.: Finding efficient circuits using SAT-solvers. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 32\u201344. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_5"},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"19_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3","volume-title":"Decision Procedures - An Algorithmic Point of View","author":"D Kroening","year":"2016","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-540-74105-3"},{"key":"19_CR28","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M., W\u00fcstholz, V.: The Dafny integrated development environment. In: Dubois, C., Giannakopoulou, D., M\u00e9ry, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014. EPTCS, Grenoble, France, 6 April 2014, vol. 149, pp. 3\u201315 (2014). https:\/\/doi.org\/10.4204\/EPTCS.149.2","DOI":"10.4204\/EPTCS.149.2"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-319-21690-4_22","volume-title":"Computer Aided Verification","author":"KRM Leino","year":"2015","unstructured":"Leino, K.R.M., W\u00fcstholz, V.: Fine-grained caching of verification results. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 380\u2013397. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_22"},{"key":"19_CR30","doi-asserted-by":"publisher","unstructured":"Madhavan, R., Kulal, S., Kuncak, V.: Contract-based resource verification for higher-order functions with memoization. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) (2017). https:\/\/doi.org\/10.1145\/3009837.3009874","DOI":"10.1145\/3009837.3009874"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-28717-6_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Merz","year":"2012","unstructured":"Merz, S., Vanzetto, H.: Automatic verification of TLA$$^+$$ proof obligations with SMT solvers. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 289\u2013303. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_23"},{"key":"19_CR32","doi-asserted-by":"publisher","unstructured":"Milovancevic, D., Kuncak, V.: Proving and disproving equivalence of functional programming assignments (artifact) (2023). https:\/\/doi.org\/10.5281\/zenodo.7810840","DOI":"10.5281\/zenodo.7810840"},{"key":"19_CR33","doi-asserted-by":"publisher","unstructured":"Milovancevic, D., Kun\u010dak, V.: Proving and disproving equivalence of functional programming assignments. In: ACM SIGPLAN Conference Programming Language Design and Implementation (PLDI) (2023). https:\/\/doi.org\/10.1145\/3591258","DOI":"10.1145\/3591258"},{"key":"19_CR34","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":"19_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-03359-9_5","volume-title":"Theorem Proving in Higher Order Logics","author":"A Naumowicz","year":"2009","unstructured":"Naumowicz, A., Korni\u0142owicz, A.: A brief overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 67\u201372. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_5"},{"key":"19_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-319-29778-1_16","volume-title":"Languages and Compilers for Parallel Computing","author":"A Prokopec","year":"2016","unstructured":"Prokopec, A., Odersky, M.: Conc-trees for functional and parallel programming. In: Shen, X., Mueller, F., Tuck, J. (eds.) LCPC 2015. LNCS, vol. 9519, pp. 254\u2013268. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29778-1_16"},{"key":"19_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E\u00a01.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_49"},{"key":"19_CR38","doi-asserted-by":"publisher","unstructured":"Song, D., Lee, W., Oh, H.: Context-aware and data-driven feedback generation for programming assignments. In: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2021, pp. 328\u2013340. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3468264.3468598","DOI":"10.1145\/3468264.3468598"},{"key":"19_CR39","unstructured":"Suter, P.: Non-clausal satisfiability modulo theories. Technical report, M.Sc. thesis, EPFL (2008). http:\/\/infoscience.epfl.ch\/record\/126445"},{"key":"19_CR40","doi-asserted-by":"publisher","unstructured":"Voirol, N., Kneuss, E., Kuncak, V.: Counter-example complete verification for higher-order functions. In: Scala Symposium (2015). https:\/\/doi.org\/10.1145\/2774975.2774978","DOI":"10.1145\/2774975.2774978"},{"key":"19_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-79876-5_24","volume-title":"Automated Deduction \u2013 CADE 28","author":"P Vukmirovi\u0107","year":"2021","unstructured":"Vukmirovi\u0107, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 415\u2013432. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_24"},{"key":"19_CR42","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10"},{"key":"19_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-71067-7_7","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"2008","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The isabelle framework. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33\u201338. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_7"},{"issue":"1","key":"19_CR44","doi-asserted-by":"publisher","first-page":"325","DOI":"10.2307\/1969001","volume":"42","author":"PM Whitman","year":"1941","unstructured":"Whitman, P.M.: Free lattices. Ann. Math. 42(1), 325\u2013330 (1941). https:\/\/doi.org\/10.2307\/1969001","journal-title":"Ann. Math."},{"key":"19_CR45","doi-asserted-by":"publisher","unstructured":"Zhang, H.T., Jiang, J.H.R., Mishchenko, A.: A circuit-based SAT solver for logic synthesis. In: 2021 IEEE\/ACM International Conference on Computer Aided Design (ICCAD), pp. 1\u20136 (2021). https:\/\/doi.org\/10.1109\/ICCAD51958.2021.9643505","DOI":"10.1109\/ICCAD51958.2021.9643505"}],"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-031-37709-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:03:54Z","timestamp":1689501834000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Paris","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":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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":"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":"11","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)"}}]}}