{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:13:51Z","timestamp":1784837631956,"version":"3.55.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"4","funder":[{"DOI":"10.13039\/501100001711","name":"Swiss National Science Foundation","doi-asserted-by":"crossref","award":["200021_197353"],"award-info":[{"award-number":["200021_197353"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001711","name":"Swiss National Science Foundation","doi-asserted-by":"crossref","award":["200021_185031"],"award-info":[{"award-number":["200021_185031"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["23-06506S"],"award-info":[{"award-number":["23-06506S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,12,31]]},"abstract":"<jats:p>Formal verification tooling increasingly relies on logic solvers as automated reasoning engines. A commonality among these solvers is the high complexity of their codebases, which makes bug occurrence disturbingly frequent. Tool competitions have showcased many examples of state-of-the-art solvers disagreeing on the satisfiability of logic formulas, be it solvers for Boolean satisfiability (SAT), satisfiability modulo theories (SMT), or constrained Horn clauses (CHC). The validation of solvers\u2019 results is thus of paramount importance, in order to increase the confidence not only in the solvers themselves but also in the tooling which they underpin. Among the formalisms commonly used by modern verification tools, CHC is one that has seen, at the same time, extensive practical usage and very little effort in result validation. We propose a two-layered validation approach for witnesses of CHC satisfiability that validates CHC models via proof-backed SMT queries. We developed a modular evaluation framework, ATHENA, and assessed the approach\u2019s viability via large scale experimentation, comparing three CHC solvers, five SMT solvers, and five proof checkers. Our results indicate that the approach is feasible, with the potential to be incorporated into CHC-based tooling, and also confirm the need for validation, with fourteen bugs being found in the tools used.<\/jats:p>\n                  <jats:p\/>","DOI":"10.1145\/3716505","type":"journal-article","created":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T06:19:33Z","timestamp":1739427573000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Validation of CHC Satisfiability with ATHENA"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1097-2367","authenticated-orcid":false,"given":"Rodrigo","family":"Otoni","sequence":"first","affiliation":[{"name":"USI Lugano","place":["Lugano, Switzerland"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8140-4098","authenticated-orcid":false,"given":"Martin","family":"Blicha","sequence":"additional","affiliation":[{"name":"USI Lugano","place":["Lugano, Switzerland"]},{"name":"Charles University","place":["Lugano, Switzerland"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3864-9078","authenticated-orcid":false,"given":"Patrick","family":"Eugster","sequence":"additional","affiliation":[{"name":"USI Lugano","place":["Lugano, Switzerland"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8872-4913","authenticated-orcid":false,"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[{"name":"USI Lugano","place":["Lugano, Switzerland"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,31]]},"reference":[{"key":"e_1_3_3_2_2","first-page":"325","volume-title":"Proceedings of the 34th International Conference on Computer Aided Verification","author":"Alt Leonardo","year":"2022","unstructured":"Leonardo Alt, Martin Blicha, Antti E. J. Hyv\u00e4rinen, and Natasha Sharygina. 2022. SolCMC: Solidity compiler\u2019s model checker. In Proceedings of the 34th International Conference on Computer Aided Verification. 325\u2013338."},{"key":"e_1_3_3_3_2","first-page":"367","volume-title":"Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Andreotti Bruno","year":"2023","unstructured":"Bruno Andreotti, Hanna Lachnitt, and Haniel Barbosa. 2023. Carcara: An efficient proof checker and elaborator for SMT proofs in the alethe format. In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 367\u2013386."},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"e_1_3_3_5_2","first-page":"59","volume-title":"Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Baek Seulkee","year":"2021","unstructured":"Seulkee Baek, Mario Carneiro, and Marijn J. H. Heule. 2021. A flexible proof format for SAT solver-elaborator communication. In Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 59\u201375."},{"key":"e_1_3_3_6_2","first-page":"415","volume-title":"Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Barbosa Haniel","year":"2022","unstructured":"Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N\u00f6tzli, et al.2022. CVC5: A versatile and industrial-strength SMT solver. In Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 415\u2013442."},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-09502-y"},{"key":"e_1_3_3_8_2","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2021. The SMT-LIB Standard: Version 2.6. Retrieved August 16 2024 from https:\/\/smtlib.cs.uiowa.edu\/papers\/smt-lib-reference-v2.6-r2021-05-12.pdf"},{"key":"e_1_3_3_9_2","doi-asserted-by":"crossref","unstructured":"Clark Barrett Roberto Sebastiani Sanjit Seshia and Cesare Tinelli. 2021. Satisfiability modulo theories. In Handbook of Satisfiability Second Edition of Frontiers in Artificial Intelligence and Applications Armin Biere Marijn J. H. Heule Hans van Maaren and Toby Walsh (Eds.). Vol. 336 825\u2013885.","DOI":"10.3233\/FAIA201017"},{"key":"e_1_3_3_10_2","first-page":"495","volume-title":"Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Beyer Dirk","year":"2023","unstructured":"Dirk Beyer. 2023. Competition on software verification and witness validation: SV-COMP 2023. In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 495\u2013522."},{"key":"e_1_3_3_11_2","first-page":"160","volume-title":"Proceedings of the 29th International Symposium on Static Analysis","author":"Beyer Dirk","year":"2022","unstructured":"Dirk Beyer and Jan Strej\u010dek. 2022. Case study on verification-witness validators: Where we are and where we go. In Proceedings of the 29th International Symposium on Static Analysis. 160\u2013174."},{"key":"e_1_3_3_12_2","first-page":"24","article-title":"Horn clause solvers for program verification","volume":"9300","author":"Bj\u00f8rner Nikolaj","year":"2015","unstructured":"Nikolaj Bj\u00f8rner, Arie Gurfinkel, Ken McMillan, and Andrey Rybalchenko. 2015. Horn clause solvers for program verification. Fields of Logic and Computation II. Lecture Notes in Computer Science 9300 (2015), 24\u201351.","journal-title":"Fields of Logic and Computation II. Lecture Notes in Computer Science"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9335-3"},{"key":"e_1_3_3_14_2","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/978-3-031-37703-7_10","volume-title":"Proceedings of the 35th International Conference on Computer Aided Verification","author":"Blicha Martin","year":"2023","unstructured":"Martin Blicha, Konstantin Britikov, and Natasha Sharygina. 2023. The golem horn solver. In Proceedings of the 35th International Conference on Computer Aided Verification. 209\u2013223."},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"e_1_3_3_16_2","first-page":"151","volume-title":"Proceedings of the 22nd International Conference on Automated Deduction","author":"Bouton Thomas","year":"2009","unstructured":"Thomas Bouton, Diego Caminha B. de Oliveira, David D\u00e9harbe, and Pascal Fontaine. 2009. veriT: An open, trustable and efficient SMT-solver. In Proceedings of the 22nd International Conference on Automated Deduction. 151\u2013156."},{"key":"e_1_3_3_17_2","unstructured":"Martin Bromberger Jochen Hoenicke and Fran\u00e7ois Bobot. 2023. SMT-COMP 2023: Competition Report. Retrieved August 16 2024 from https:\/\/smt-workshop.cs.uiowa.edu\/2023\/slides\/smtcomp.pdf"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"e_1_3_3_19_2","first-page":"32","volume-title":"Proceedings of the 19th International Workshop on Satisfiability Modulo Theories","author":"Bury Guillaume","year":"2021","unstructured":"Guillaume Bury. 2021. Dolmen: A validator for SMT-LIB and much more. In Proceedings of the 19th International Workshop on Satisfiability Modulo Theories. 32\u201339."},{"key":"e_1_3_3_20_2","first-page":"47","volume-title":"Proceedings of the 1st IEEE European Symposium on Security and Privacy","author":"Calzavara Stefano","year":"2016","unstructured":"Stefano Calzavara, Ilya Grishchenko, and Matteo Maffei. 2016. HornDroid: Practical and sound static analysis of android applications by SMT solving. In Proceedings of the 1st IEEE European Symposium on Security and Privacy. 47\u201362."},{"key":"e_1_3_3_21_2","first-page":"248","volume-title":"Proceedings of the 19th International SPIN Workshop","author":"Christ J\u00fcrgen","year":"2012","unstructured":"J\u00fcrgen Christ, Jochen Hoenicke, and Alexander Nutz. 2012. SMTInterpol: An interpolating SMT solver. In Proceedings of the 19th International SPIN Workshop. 248\u2013254."},{"key":"e_1_3_3_22_2","first-page":"220","volume-title":"Proceedings of the 26th International Conference on Automated Deduction","author":"Cruz-Filipe Lu\u00eds","year":"2017","unstructured":"Lu\u00eds Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider-Kamp. 2017. Efficient certified RAT verification. In Proceedings of the 26th International Conference on Automated Deduction. 220\u2013236."},{"key":"e_1_3_3_23_2","first-page":"123","volume-title":"Proceedings of the 7th International Workshop on the Implementation of Logics","author":"Moura Leonardo de","year":"2008","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Proofs and refutations, and Z3. In Proceedings of the 7th International Workshop on the Implementation of Logics. 123\u2013132."},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_25_2","first-page":"42","volume-title":"Proceedings of the 6th Workshop on Horn Clauses for Verification and Synthesis","author":"Dietsch Daniel","year":"2019","unstructured":"Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, and Andreas Podelski. 2019. Ultimate TreeAutomizer (CHC-COMP tool description). In Proceedings of the 6th Workshop on Horn Clauses for Verification and Synthesis. 42\u201347."},{"key":"e_1_3_3_26_2","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-319-63390-9_7","volume-title":"Proceedings of the 29th International Conference on Computer Aided Verification","author":"Ekici Burak","year":"2017","unstructured":"Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett. 2017. SMTCoq: A plug-in for integrating SMT solvers into coq. In Proceedings of the 29th International Conference on Computer Aided Verification. 126\u2013133."},{"key":"e_1_3_3_27_2","first-page":"559","volume-title":"Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Ernst Gidon","year":"2023","unstructured":"Gidon Ernst. 2023. Korn - software verification with horn clauses (competition contribution). In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 559\u2013564."},{"key":"e_1_3_3_28_2","unstructured":"Gidon Ernst and Jos\u00e9 F. Morales. 2024. CHC-COMP 2024: Competition Report. Retrieved August 16 2024 from https:\/\/chc-comp.github.io\/2024\/CHC-COMP_2024_Report-HCSV.pdf"},{"key":"e_1_3_3_29_2","first-page":"167","volume-title":"Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Fontaine Pascal","year":"2006","unstructured":"Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, and Alwen Tiu. 2006. Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 167\u2013181."},{"key":"e_1_3_3_30_2","doi-asserted-by":"crossref","first-page":"712","DOI":"10.1007\/978-3-031-10769-6_41","volume-title":"Proceedings of the 11th International Joint Conference on Automated Reasoning","author":"Frohn Florian","year":"2022","unstructured":"Florian Frohn and J\u00fcrgen Giesl. 2022. Proving non-termination and lower runtime bounds with LoAT (system description). In Proceedings of the 11th International Joint Conference on Automated Reasoning. 712\u2013722."},{"key":"e_1_3_3_31_2","first-page":"1","volume-title":"Proceedings of the 13th International Workshop on Satisfiability Modulo Theories","author":"Gario Marco","year":"2015","unstructured":"Marco Gario and Andrea Micheli. 2015. PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms. In Proceedings of the 13th International Workshop on Satisfiability Modulo Theories. 1\u201310."},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC49474.2019.00010"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","unstructured":"Matthias Heizmann Daniel Dietsch Jochen Hoenicke Alexander Nutz Andreas Podelski and Frank Sch\u00fcssele. 2024. Ultimate Unihorn - Solver Description. DOI:10.4204\/EPTCS.402.10. Page 99.","DOI":"10.4204\/EPTCS.402.10"},{"key":"e_1_3_3_36_2","first-page":"181","volume-title":"Proceedings of the 13th Conference on Formal Methods in Computer-Aided Design","author":"Heule Marijn J.H.","year":"2013","unstructured":"Marijn J.H. Heule, Warren A. Hunt, and Nathan Wetzler. 2013. Trimming while checking clausal proofs. In Proceedings of the 13th Conference on Formal Methods in Computer-Aided Design. 181\u2013188."},{"key":"e_1_3_3_37_2","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/978-3-319-66107-0_18","volume-title":"Proceedings of the 8th International Conference on Interactive Theorem Proving","author":"Heule Marijn J. H.","year":"2017","unstructured":"Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Nathan Wetzler. 2017. Efficient, verified checking of propositional proofs. In Proceedings of the 8th International Conference on Interactive Theorem Proving. 269\u2013284."},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_3_40_2","first-page":"54","volume-title":"Proceedings of the 20th International Workshop on Satisfiability Modulo Theories","author":"Hoenicke Jochen","year":"2022","unstructured":"Jochen Hoenicke and Tanja Schindler. 2022. A simple proof format for SMT. In Proceedings of the 20th International Workshop on Satisfiability Modulo Theories. 54\u201370."},{"key":"e_1_3_3_41_2","first-page":"39","volume-title":"Proceedings of the 1st Workshop on Horn Clauses for Verification and Synthesis","author":"Hojjat Hossein","year":"2014","unstructured":"Hossein Hojjat, Philipp R\u00fcmmer, Pavle Subotic, and Wang Yi. 2014. Horn clauses for communicating timed systems. In Proceedings of the 1st Workshop on Horn Clauses for Verification and Synthesis. 39\u201352."},{"key":"e_1_3_3_42_2","first-page":"1","volume-title":"Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design","author":"Hojjat Hossein","year":"2018","unstructured":"Hossein Hojjat and Philipp R\u00fcmmer. 2018. The eldarica horn solver. In Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design. 1\u20137."},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0249-4"},{"key":"e_1_3_3_45_2","volume-title":"Decision Procedures - An Algorithmic Point of View (2nd. ed.)","author":"Kroening Daniel","year":"2016","unstructured":"Daniel Kroening and Ofer Strichman. 2016. Decision Procedures - An Algorithmic Point of View (2nd. ed.). Springer Berlin."},{"key":"e_1_3_3_46_2","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1145\/2535838.2535841","volume-title":"Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Kumar Ramana","year":"2014","unstructured":"Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A verified implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 179\u2013191."},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09525-z"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18074.2021.9586272"},{"key":"e_1_3_3_50_2","first-page":"62","volume-title":"Proceedings of the 18th International Conference on integrated Formal Methods","author":"Otoni Rodrigo","year":"2023","unstructured":"Rodrigo Otoni, Martin Blicha, Patrick Eugster, and Natasha Sharygina. 2023. CHC model validation with proof guarantees. In Proceedings of the 18th International Conference on integrated Formal Methods. 62\u201381."},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3564699"},{"key":"e_1_3_3_52_2","first-page":"329","volume-title":"Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Reeves Joseph E.","year":"2023","unstructured":"Joseph E. Reeves, Benjamin Kiesl-Reiter, and Marijn J. H. Heule. 2023. Propositional proof skeletons. In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 329\u2013347."},{"key":"e_1_3_3_53_2","unstructured":"Andrew Reynolds and Hans-J\u00f6rg Schurr. 2024. AletheLF Checker (alfc). Retrieved August 16 2024 from https:\/\/cvc5.github.io\/docs\/cvc5-1.1.2\/proofs\/output_alf.html"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0219-7"},{"key":"e_1_3_3_55_2","doi-asserted-by":"crossref","first-page":"444","DOI":"10.1007\/978-3-319-66107-0_28","volume-title":"Proceedings of the 8th International Conference on Interactive Theorem Proving","author":"Ericsson Adam Sandberg","year":"2017","unstructured":"Adam Sandberg Ericsson, Magnus O. Myreen, and Johannes \u00c5man Pohjola. 2017. A verified generational garbage collector for CakeML. In Proceedings of the 8th International Conference on Interactive Theorem Proving. 444\u2013461."},{"key":"e_1_3_3_56_2","first-page":"49","volume-title":"Proceedings of the 7th Workshop on Proof eXchange for Theorem Proving","author":"Schurr Hans-J\u00f8rg","year":"2021","unstructured":"Hans-J\u00f8rg Schurr, Mathias Fleury, Haniel Barbosa, and Pascal Fontaine. 2021. Alethe: Towards a generic SMT proof format. In Proceedings of the 7th Workshop on Proof eXchange for Theorem Proving. 49\u201354."},{"key":"e_1_3_3_57_2","first-page":"600","volume-title":"Proceedings of the 1st International Symposium on Computer Science in Russia","author":"Sinz Carsten","year":"2006","unstructured":"Carsten Sinz and Armin Biere. 2006. Extended resolution proofs for conjoining BDDs. In Proceedings of the 1st International Symposium on Computer Science in Russia. 600\u2013611."},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0163-3"},{"issue":"1","key":"e_1_3_3_59_2","first-page":"42","article-title":"GNU parallel - the command-line power tool","volume":"36","author":"Tange Ole","year":"2011","unstructured":"Ole Tange. 2011. GNU parallel - the command-line power tool. ;login: The USENIX Magazine 36, 1 (2011), 42\u201347.","journal-title":";login: The USENIX Magazine"},{"key":"e_1_3_3_60_2","first-page":"176","volume-title":"Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design","author":"T\u00f3th Tam\u00e1s","year":"2017","unstructured":"Tam\u00e1s T\u00f3th, \u00c1kos Hajdu, Andr\u00e1s V\u00f6r\u00f6s, Zolt\u00e1n Micskei, and Istv\u00e1n Majzik. 2017. Theta: A framework for abstraction refinement-based model checking. In Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design. 176\u2013179."},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_31"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3716505","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:07:28Z","timestamp":1761919648000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3716505"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,31]]},"references-count":60,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12,31]]}},"alternative-id":["10.1145\/3716505"],"URL":"https:\/\/doi.org\/10.1145\/3716505","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,31]]},"assertion":[{"value":"2024-08-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-04","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-31","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}