{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T14:05:15Z","timestamp":1779372315853,"version":"3.53.1"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T00:00:00Z","timestamp":1773878400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T00:00:00Z","timestamp":1773878400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Albert-Ludwigs-Universit\u00e4t Freiburg im Breisgau"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2026,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Using Symbolic Computer Algebra (SCA) enabled a huge progress in formal verification of arithmetic circuits in recent years. Several different approaches have been proposed showing great success especially for the verification of multipliers. Some of them are based on precomputing and simplifying polynomials for specific circuit structures like converging cones while others take advantage of known or detected hierarchy information to replace and simplify particular subcircuits of the design. In this paper we propose a new method that avoids the use of such methods and applies only two dynamic approaches: (1) choosing a good substitution order for the backward rewriting process and (2) adjusting the phases of signals occurring in the intermediate polynomials during the verification process. Both methods are simply based on a greedy local search taking the sizes of intermediate polynomials into account. Our experimental results show that this method is very competitive with already existing tools and it improves their robustness, e.g. against optimizations of the verified circuits using logic synthesis.<\/jats:p>","DOI":"10.1007\/s10703-026-00494-9","type":"journal-article","created":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T09:15:44Z","timestamp":1773911744000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic computer algebra for multipliers revisited - demonstrating the significance of order and phase optimization"],"prefix":"10.1007","volume":"68","author":[{"given":"Alexander","family":"Konrad","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,3,19]]},"reference":[{"key":"494_CR1","unstructured":"(2019) ABC: a system for sequential synthesis and verification. Available at https:\/\/people.eecs.berkeley.edu\/alanmi\/abc\/"},{"issue":"10","key":"494_CR2","first-page":"547","volume":"26","author":"B Becker","year":"1990","unstructured":"Becker B, Hartmann J (1990) Optimal-time multipliers and c-testability. J Inf Process Cybern 26(10):547\u2013561","journal-title":"J Inf Process Cybern"},{"issue":"2","key":"494_CR3","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1093\/qjmam\/4.2.236","volume":"4","author":"AD Booth","year":"1951","unstructured":"Booth AD (1951) A signed binary multiplication technique. Q J Mech Appl Math 4(2):236\u2013240","journal-title":"Q J Mech Appl Math"},{"key":"494_CR4","doi-asserted-by":"crossref","unstructured":"Brayton RK, Mishchenko A (2010) ABC: an academic industrial-strength verification tool. In: Computer aided verification, pp 24\u201340","DOI":"10.1007\/978-3-642-14295-6_5"},{"issue":"3","key":"494_CR5","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1109\/TC.1982.1675982","volume":"31","author":"RP Brent","year":"1982","unstructured":"Brent RP, Kung HT (1982) A regular layout for parallel adders. IEEE Comput 31(3):260\u2013264","journal-title":"IEEE Comput"},{"issue":"8","key":"494_CR6","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comp 35(8):677\u2013691","journal-title":"IEEE Trans Comp"},{"issue":"2","key":"494_CR7","first-page":"137","volume":"3","author":"RE Bryant","year":"2001","unstructured":"Bryant RE, Chen Y (2001) Verification of arithmetic circuits using binary moment diagrams. Softw Tools Technol Transf 3(2):137\u2013155","journal-title":"Softw Tools Technol Transf"},{"key":"494_CR8","doi-asserted-by":"crossref","unstructured":"Bryant RE, Chen YA (1995) Verification of arithmetic circuits with binary moment diagrams. In: Design automation conf., pp 535\u2013541","DOI":"10.1145\/217474.217583"},{"key":"494_CR9","doi-asserted-by":"crossref","unstructured":"Burch JR (1991) Using BDDs to verify multipliers. In: Design automation conf., pp 408\u2013412","DOI":"10.1145\/127601.127703"},{"key":"494_CR10","doi-asserted-by":"crossref","unstructured":"Ciesielski M, Yu C, Liu D et al. (2015) Verification of gate-level arithmetic circuits by function extraction. In: Design automation conf., pp 52:1\u201352:6","DOI":"10.1145\/2744769.2744925"},{"issue":"4","key":"494_CR11","first-page":"129","volume":"20","author":"T Coe","year":"1995","unstructured":"Coe T (1995) Inside the pentium FDIV bug. Dr Dobbs J 20(4):129\u2013135","journal-title":"Dr Dobbs J"},{"key":"494_CR12","first-page":"349","volume":"34","author":"L Dadda","year":"1965","unstructured":"Dadda L (1965) Some schemes for parallel multipliers. Alta Frequenza 34:349\u2013356","journal-title":"Alta Frequenza"},{"key":"494_CR13","first-page":"2","volume-title":"K*BMDs: a new data structure for verification","author":"R Drechsler","year":"1996","unstructured":"Drechsler R, Becker B, Ruppertz S (1996) K*BMDs: a new data structure for verification. In: European design & test conf., IEEE Computer Society, pp 2\u20138"},{"issue":"2","key":"494_CR14","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.micpro.2015.01.007","volume":"39","author":"F Farahmandi","year":"2015","unstructured":"Farahmandi F, Alizadeh B (2015) Gr\u00f6bner basis based formal verification of large arithmetic circuits using gaussian elimination and cone-based polynomial extraction. Microprocess Microsys 39(2):83\u201396","journal-title":"Microprocess Microsys"},{"key":"494_CR15","doi-asserted-by":"crossref","unstructured":"Goldberg EI, Prasad MR, Brayton RK (2001) Using SAT for combinational equivalence checking. In: Design, automation and test in Europe, IEEE Computer Society, pp 114\u2013121","DOI":"10.1109\/DATE.2001.915010"},{"key":"494_CR16","doi-asserted-by":"crossref","unstructured":"Hamaguchi K, Morita A, Yajima S (1995) Efficient construction of binary moment diagrams for verifying arithmetic circuits. In: International conference on computer-aided design, pp 78\u201382","DOI":"10.1109\/ICCAD.1995.479995"},{"key":"494_CR17","doi-asserted-by":"publisher","first-page":"3500","DOI":"10.1093\/ietfec\/e89-a.12.3500","volume":"89-A","author":"N Homma","year":"2006","unstructured":"Homma N, Watanabe Y, Aoki T et al. (2006) Formal design of arithmetic circuits based on arithmetic description language. IEICE Trans Fundam 89-A:3500\u20133509","journal-title":"IEICE Trans Fundam"},{"key":"494_CR18","doi-asserted-by":"crossref","unstructured":"H\u00f6reth S, Drechsler R (1998) Dynamic minimization of word-level decision diagrams. In: Design, automation and test in Europe, IEEE Computer Society, pp 612\u2013617","DOI":"10.1109\/DATE.1998.655921"},{"key":"494_CR19","doi-asserted-by":"publisher","first-page":"20150399","DOI":"10.1098\/rsta.2015.0399","volume":"375","author":"W Hunt","year":"2017","unstructured":"Hunt W, Kaufmann M, Moore J et al. (2017) Industrial hardware and software verification with ACL2. Philos Trans R Soc A 375:20150399","journal-title":"Philos Trans R Soc A"},{"key":"494_CR20","doi-asserted-by":"crossref","unstructured":"Kaufmann D, Biere A (2021) Amulet 2.0 for verifying multiplier circuits. In: Tools and algorithms for the construction and analysis of systems. Springer, pp 357\u2013364","DOI":"10.1007\/978-3-030-72013-1_19"},{"key":"494_CR21","doi-asserted-by":"publisher","unstructured":"Kaufmann D, Biere A (2022) Fuzzing and delta debugging and-inverter graph verification tools. In: Kov\u00e1cs L, Meinke K (eds) Tests and proofs - 16th international conference, TAP 2022, Lecture Notes in Computer Science, vol 13361. Springer, pp 69\u201388. https:\/\/doi.org\/10.1007\/978-3-031-09827-7_5","DOI":"10.1007\/978-3-031-09827-7_5"},{"issue":"2","key":"494_CR22","first-page":"133","volume":"25","author":"D Kaufmann","year":"2023","unstructured":"Kaufmann D, Biere A (2023) Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra. Softw Tools Technol Transf 25(2):133\u2013144","journal-title":"Softw Tools Technol Transf"},{"key":"494_CR23","doi-asserted-by":"crossref","unstructured":"Kaufmann D, Biere A, Kauers M (2019) Verifying large multipliers by combining SAT and computer algebra. In: Int\u2019l conf. on formal methods in CAD, pp 28\u201336","DOI":"10.23919\/FMCAD.2019.8894250"},{"key":"494_CR24","unstructured":"Kaufmann D, Fleury M, Biere A (2020) The proof checkers pacheck and past\u00e8que for the practical algebraic calculus. In: Int\u2019l conf. on formal methods in CAD, IEEE, pp 264\u2013269"},{"key":"494_CR25","doi-asserted-by":"crossref","unstructured":"Kaufmann D, Beame P, Biere A et al. (2022) Adding dual variables to algebraic reasoning for gate-level multiplier verification. In: Design, automation and test in Europe, IEEE","DOI":"10.23919\/DATE54114.2022.9774587"},{"issue":"1","key":"494_CR26","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10703-022-00391-x","volume":"64","author":"D Kaufmann","year":"2024","unstructured":"Kaufmann D, Fleury M, Biere A et al. (2024) Practical algebraic calculus and nullstellensatz with the checkers pacheck and past\u00e8que and nuss-checker. Form Methods Syst Des Int J 64(1):73\u2013107. https:\/\/doi.org\/10.1007\/s10703-022-00391-x","journal-title":"An Int J"},{"issue":"1","key":"494_CR27","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1023\/A:1021752130394","volume":"22","author":"M Keim","year":"2003","unstructured":"Keim M, Drechsler R, Becker B et al. (2003) Polynomial formal verification of multipliers. Form Methods Syst Des 22(1):39\u201358","journal-title":"Form Methods Syst Des"},{"issue":"8","key":"494_CR28","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1109\/TC.1973.5009159","volume":"22","author":"PM Kogge","year":"1973","unstructured":"Kogge PM, Stone HS (1973) A parallel algorithm for the efficient solution of a general class of recurrence equations. IEEE Comput 22(8):786\u2013793","journal-title":"IEEE Comput"},{"key":"494_CR29","unstructured":"Konrad A, Scholl C (2024) Benchmarks, binaries and experimental data. https:\/\/abs.informatik.uni-freiburg.de\/src\/projects_view.php?projectID=24"},{"key":"494_CR30","doi-asserted-by":"publisher","unstructured":"Konrad A, Scholl C (2024) Symbolic computer algebra for multipliers revisited - it\u2019s all about orders and phases. In: Int\u2019l conf. on formal methods in CAD, TU Wien Academic Press, pp 261\u2013271. https:\/\/doi.org\/10.34727\/2024\/isbn.978-3-85448-065-5_32","DOI":"10.34727\/2024\/isbn.978-3-85448-065-5_32"},{"key":"494_CR31","unstructured":"Konrad A, Scholl C, Mahzoon A et al. (2022) Divider verification using symbolic computer algebra and delayed don\u2019t care optimization. In: Int\u2019l conf. on formal methods in CAD, IEEE, pp 1\u201310"},{"key":"494_CR32","volume-title":"Computer arithmetic algorithms","author":"I Koren","year":"2001","unstructured":"Koren I (2001) Computer arithmetic algorithms, 2nd edn. A. K. Peters, Ltd","edition":"2nd edn"},{"issue":"4","key":"494_CR33","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1145\/322217.322232","volume":"27","author":"RE Ladner","year":"1980","unstructured":"Ladner RE, Fischer MJ (1980) Parallel prefix computation. J ACM 27(4):831\u2013838","journal-title":"J Acm"},{"issue":"9","key":"494_CR34","doi-asserted-by":"publisher","first-page":"1409","DOI":"10.1109\/TCAD.2013.2259540","volume":"32","author":"J Lv","year":"2013","unstructured":"Lv J, Kalla P, Enescu F (2013) Efficient Gr\u00f6bner basis reductions for formal verification of Galois field arithmetic circuits. IEEE Trans Intell Transp Syst Comput Aided Des Circuits Syst 32(9):1409\u20131420","journal-title":"IEEE Trans Intell Transp Syst Comput Aided Des Circuits Syst"},{"key":"494_CR35","doi-asserted-by":"crossref","unstructured":"Mahzoon A, Gro\u00dfe D, Drechsler R (2018) PolyCleaner: clean your polynomials before backward rewriting to verify million-gate multipliers. Int Conf Comput-Aided Des, pp 129:1\u2013129:8","DOI":"10.1145\/3240765.3240837"},{"key":"494_CR36","doi-asserted-by":"crossref","unstructured":"Mahzoon A, Gro\u00dfe D, Drechsler R (2019) RevSCA: using reverse engineering to bring light into backward rewriting for big and dirty multipliers. In: Design automation conf., pp 185:1\u2013185:6","DOI":"10.1145\/3316781.3317898"},{"key":"494_CR37","doi-asserted-by":"crossref","unstructured":"Mahzoon A, Gro\u00dfe D, Scholl C et al. (2020) Towards formal verification of optimized and industrial multipliers. In: Design, automation and test in Europe, pp 544\u2013549","DOI":"10.23919\/DATE48585.2020.9116485"},{"key":"494_CR38","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-030-68071-8_9","volume-title":"Recent findings in boolean techniques","author":"A Mahzoon","year":"2021","unstructured":"Mahzoon A, Gro\u00dfe D, Drechsler R (2021) GenMul: generating architecturally complex multipliers to challenge formal verification tools. In: Drechsler R, Gro\u00dfe D (eds) Recent findings in boolean techniques. Springer International Publishing, pp 177\u2013191"},{"issue":"5","key":"494_CR39","doi-asserted-by":"publisher","first-page":"1573","DOI":"10.1109\/TCAD.2021.3083682","volume":"41","author":"A Mahzoon","year":"2022","unstructured":"Mahzoon A, Gro\u00dfe D, Drechsler R (2022) RevSCA-2.0: SCA-based formal verification of nontrivial multipliers using reverse engineering and local vanishing removal. IEEE Trans Intell Transp Syst Comput Aided Des Circuits Syst 41(5):1573\u20131586","journal-title":"IEEE Trans Intell Transp Syst Comput Aided Des Circuits Syst"},{"key":"494_CR40","doi-asserted-by":"crossref","unstructured":"Mahzoon A, Gro\u00dfe D, Scholl C et al. (2022) Formal verification of modular multipliers using symbolic computer algebra and boolean satisfiability. In: Design automation conf.","DOI":"10.1145\/3489517.3530605"},{"key":"494_CR41","unstructured":"Mahzoon A, Gro\u00dfe D, Drechsler R (2023) Genmul. https:\/\/ics.jku.at\/research\/sca-verification\/genmul\/"},{"key":"494_CR42","doi-asserted-by":"crossref","unstructured":"Ritirc D, Biere A, Kauers M (2017) Column-wise verification of multipliers using computer algebra. In: Int\u2019l conf. on formal methods in CAD, pp 23\u201330","DOI":"10.23919\/FMCAD.2017.8102237"},{"key":"494_CR43","doi-asserted-by":"crossref","unstructured":"Ritirc D, Biere A, Kauers M (2018) Improving and extending the algebraic approach for verifying gate-level multipliers. In: Design, automation and test in Europe, pp 1556\u20131561","DOI":"10.23919\/DATE.2018.8342263"},{"key":"494_CR44","doi-asserted-by":"crossref","unstructured":"Sayed-Ahmed A, Gro\u00dfe D, K\u00fchne U et al. (2016) Formal verification of integer multipliers by combining Gr\u00f6bner basis with logic reduction. In: Design, automation and test inEurope, pp 1048\u20131053","DOI":"10.3850\/9783981537079_0248"},{"key":"494_CR45","doi-asserted-by":"crossref","unstructured":"Sayed-Ahmed AAR, Gro\u00dfe D, Soeken M et al. (2016) Equivalence checking using gr\u00f6bner bases. In: Int\u2019l conf. on formal methods in CAD, IEEE, pp 169\u2013176","DOI":"10.1109\/FMCAD.2016.7886676"},{"key":"494_CR46","doi-asserted-by":"crossref","unstructured":"Scholl C, Konrad A (2020) Symbolic computer algebra and SAT based information forwarding for fully automatic divider verification. In: Design automation conf.","DOI":"10.1109\/DAC18072.2020.9218721"},{"key":"494_CR47","doi-asserted-by":"crossref","unstructured":"Scholl C, Konrad A, Mahzoon A et al. (2021) Verifying dividers using symbolic computer algebra and don\u2019t care optimization. In: Design, automation and test in Europe, IEEE, pp 1110\u20131115","DOI":"10.23919\/DATE51398.2021.9474019"},{"key":"494_CR48","unstructured":"Silva JPM, Glass T (1999) Combinational equivalence checking using satisfiability and recursive learning. In: Design, automation and test in Europe, IEEE Computer Society \/ ACM, pp 145\u2013149"},{"key":"494_CR49","unstructured":"Temel M (2019) Fast multplier generator multgen. https:\/\/github.com\/temelmertcan\/multgen"},{"key":"494_CR50","doi-asserted-by":"crossref","unstructured":"Temel M (2024) Vescmul: verified implementation of S-C-Rewriting for multiplier verification. In: Tools and algorithms for the construction and analysis of systems. Springer, pp 340\u2013349","DOI":"10.1007\/978-3-031-57246-3_19"},{"key":"494_CR51","unstructured":"Temel M, Hunt WA (2021) Sound and automated verification of real-world RTL multipliers. In: Int\u2019l conf. on formal methods in CAD, IEEE, pp 53\u201362"},{"key":"494_CR52","doi-asserted-by":"crossref","unstructured":"Temel M, Slobodov\u00e1 A, Hunt WA (2020) Automated and scalable verification of integer multipliers. In: Computer aided verification, pp 485\u2013507","DOI":"10.1007\/978-3-030-53288-8_23"},{"key":"494_CR53","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/PGEC.1964.263830","volume":"EC-13","author":"CS Wallace","year":"1964","unstructured":"Wallace CS (1964) A suggestion for a fast multiplier. IEEE Trans Electron Comp EC-13:14\u201317","journal-title":"IEEE Trans Electron Comp"},{"key":"494_CR54","doi-asserted-by":"crossref","unstructured":"Wienand O, Wedler M, Stoffel D et al. (2008) An algebraic approach for proving data correctness in arithmetic data paths. In: Computer aided verification, pp 473\u2013486","DOI":"10.1007\/978-3-540-70545-1_45"},{"key":"494_CR55","doi-asserted-by":"crossref","unstructured":"Yasin A, Su T, Pillement S et al. (2019) Formal verification of integer dividers: division by a constant. In: IEEE annual symposium on VLSI, pp 76\u201381","DOI":"10.1109\/ISVLSI.2019.00022"},{"key":"494_CR56","first-page":"257","volume-title":"Functional verification of hardware dividers using algebraic model","author":"A Yasin","year":"2019","unstructured":"Yasin A, Su T, Pillement S et al. (2019) Functional verification of hardware dividers using algebraic model. In: VLSI of system-on-chip, pp 257\u2013262"},{"issue":"12","key":"494_CR57","doi-asserted-by":"publisher","first-page":"2131","DOI":"10.1109\/TCAD.2016.2547898","volume":"35","author":"C Yu","year":"2016","unstructured":"Yu C, Brown W, Liu D et al. (2016) Formal verification of arithmetic circuits by function extraction. IEEE Trans Intell Transp Syst Comput Aided Des Circuits Syst 35(12):2131\u20132142","journal-title":"IEEE Trans Intell Transp Syst Comput Aided Des Circuits Syst"},{"issue":"9","key":"494_CR58","doi-asserted-by":"publisher","first-page":"1907","DOI":"10.1109\/TCAD.2017.2772854","volume":"37","author":"C Yu","year":"2017","unstructured":"Yu C, Ciesielski M, Mishchenko A (2017) Fast algebraic rewriting based on and-inverter graphs. IEEE Trans Intell Transp Syst Comput Aided Des Circuits Syst 37(9):1907\u20131911","journal-title":"IEEE Trans Intell Transp Syst Comput Aided Des Circuits Syst"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-026-00494-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-026-00494-9","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-026-00494-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T13:07:23Z","timestamp":1779368843000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-026-00494-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,19]]},"references-count":58,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,4]]}},"alternative-id":["494"],"URL":"https:\/\/doi.org\/10.1007\/s10703-026-00494-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,19]]},"assertion":[{"value":"6 March 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 March 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 March 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 April 2026","order":5,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":6,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The original version of this article was revised: Example 2 in this article prematurely ended after \u2018(numbers of terms)\u2019. The following paragraph, starting with \u2018Backward rewriting proceeds in reverse topological order\u2019 and ending with \u2018and makes the backward rewriting much more robust.\u2019 has been added to Example 2.","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"6"}}