{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T11:16:21Z","timestamp":1783509381057,"version":"3.55.0"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986819","type":"print"},{"value":"9783031986826","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We present\n                    <jats:sc>PyCaliper<\/jats:sc>\n                    : a Python-embedded framework to formulate, verify, and auto-synthesize specifications for hardware designs at the register transfer level (RTL). By being Python-embedded,\n                    <jats:sc>PyCaliper<\/jats:sc>\n                    is easy to use and benefits from object-oriented principles and Python\u2019s rich ecosystem. Further,\n                    <jats:sc>PyCaliper<\/jats:sc>\n                    is a common platform that integrates novel research techniques such as specification synthesis and mature, industry-scale tooling, thus allowing them to benefit from each other. We discuss the system and implementation of\n                    <jats:sc>PyCaliper<\/jats:sc>\n                    and demonstrate its use in two case studies: in the first we compare a custom verification backend with a commercial tool and gain insights about the former, and in the second we demonstrate invariant synthesis for an RTL design.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-98682-6_21","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:15:08Z","timestamp":1753154108000},"page":"408-425","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["$$\\mathbf{{\\textsc {PyCaliper}}}$$: Python-Embedded Infrastructure for\u00a0RTL Verification and\u00a0Specification Synthesis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7704-304X","authenticated-orcid":false,"given":"Adwait","family":"Godbole","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8997-8704","authenticated-orcid":false,"given":"Brian","family":"Huffman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8355-7028","authenticated-orcid":false,"given":"Fangfei","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-5562-0365","authenticated-orcid":false,"given":"Carlos V","family":"Rozas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6190-8707","authenticated-orcid":false,"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"21_CR1","unstructured":"IEEE Standard for SystemVerilog\u2013Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800-2017 (Revision of IEEE Std 1800-2012), pp. 1\u20131315 (2018)"},{"key":"21_CR2","unstructured":"Aaron Shappell: tage-predictor (2024). GitHub repository, https:\/\/github.com\/aaronshappell\/tage-predictor"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013, pp. 1\u20138. IEEE (2013). https:\/\/ieeexplore.ieee.org\/document\/6679385\/","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Appel, A.W., et al.: Position paper: the science of deep specification. Philos. Trans. Roy. Soc. A: Math. Phys. Eng. Sci. 375(2104), 20160331 (2017). https:\/\/royalsocietypublishing.org\/doi\/abs\/10.1098\/rsta.2016.0331","DOI":"10.1098\/rsta.2016.0331"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Baaij, C., Kooijman, M., Kuper, J., Boeijink, A., Gerards, M.: C$$\\lambda $$ash: structural descriptions of synchronous hardware using haskell. In: 2010 13th Euromicro Conference on Digital System Design: Architectures, Methods and Tools, pp. 714\u2013721 (2010)","DOI":"10.1109\/DSD.2010.21"},{"key":"21_CR6","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chap.\u00a026, pp. 825\u2013885. IOS Press (2009)"},{"key":"21_CR7","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: the Calculus of Inductive Constructions. Springer, Cham (2013)"},{"issue":"4","key":"21_CR8","doi-asserted-by":"publisher","first-page":"813","DOI":"10.1145\/325478.325518","volume":"21","author":"M Blume","year":"1999","unstructured":"Blume, M., Appel, A.W.: Hierarchical modularity. ACM Trans. Program. Lang. Syst. 21(4), 813\u2013847 (1999). https:\/\/doi.org\/10.1145\/325478.325518","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI\u201911, pp. 70\u201387. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"21_CR10","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 1\u201314. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_1","DOI":"10.1007\/978-3-642-31612-8_1"},{"issue":"4\u20135","key":"21_CR11","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"AR Bradley","year":"2008","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Aspects Comput. 20(4\u20135), 379\u2013405 (2008). https:\/\/doi.org\/10.1007\/s00165-008-0080-9","journal-title":"Formal Aspects Comput."},{"key":"21_CR12","doi-asserted-by":"publisher","unstructured":"Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"21_CR13","unstructured":"Cadence: Jasper FPV App (2024). https:\/\/www.cadence.com\/en_US\/home\/tools\/system-design-and-verification\/formal-and-static-verification\/jasper-verification-platform\/formal-property-verification-app.html"},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Choi, J., Vijayaraghavan, M., Sherman, B., Chlipala, A., Arvind: Kami: a platform for high-level parametric hardware specification and its modular verification. Proc. ACM Program. Lang. 1(ICFP) (2017). https:\/\/doi.org\/10.1145\/3110268","DOI":"10.1145\/3110268"},{"key":"21_CR15","unstructured":"Claire Wolf, et. al.: Symbiyosys (2022). https:\/\/github.com\/YosysHQ\/sby"},{"key":"21_CR16","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing. PODC \u201986, pp. 240\u2013248. Association for Computing Machinery, New York, NY, USA (1986). https:\/\/doi.org\/10.1145\/10590.10611","DOI":"10.1145\/10590.10611"},{"issue":"6","key":"21_CR17","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"key":"21_CR18","unstructured":"cocotb: cocotb (2024). https:\/\/www.cocotb.org\/, https:\/\/docs.cocotb.org\/en\/stable\/#"},{"key":"21_CR19","unstructured":"diffblue: EBMC: Enhanced Bounded Model Checker (2024). GitHub repository, https:\/\/www.cprover.org\/ebmc\/, https:\/\/github.com\/diffblue\/hw-cbmc"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity. FME \u201901, pp. 500\u2013517. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45251-6_29"},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Godbole, A., Cheang, K., Manerkar, Y.A., Seshia, S.A.: Lifting micro-update models from RTL for formal security analysis. In: Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. ASPLOS \u201924, vol. 2, pp. 631\u2013648. Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3620665.3640418","DOI":"10.1145\/3620665.3640418"},{"key":"21_CR22","doi-asserted-by":"publisher","unstructured":"Godbole, A., Ye, L., Manerkar, Y.A., Seshia, S.A.: Modelling and verification of security-oriented resource partitioning schemes. In: Nadel, A., Rozier, K.Y. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, 24\u201327 October 2023, pp. 268\u2013273. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/isbn.978-3-85448-060-0_35","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_35"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-030-45190-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Part I","author":"A Goel","year":"2020","unstructured":"Goel, A., Sakallah, K.A.: AVR: abstractly verifying reachability. In: Biere, A., Parker, D. (eds.) TACAS 2020, Part I. LNCS, vol. 12078, pp. 413\u2013422. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_23"},{"key":"21_CR24","unstructured":"Intel Corporation: Branch Target Injection \/ CVE-2017-5715 \/ INTEL-SA-00088 (2018). Intel Advisory. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/software-security-guidance\/advisory-guidance\/branch-target-injection.html"},{"key":"21_CR25","doi-asserted-by":"publisher","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering. ICSE \u201910, vol. 1, pp. 215\u2013224. Association for Computing Machinery, New York, NY, USA (2010). https:\/\/doi.org\/10.1145\/1806799.1806833","DOI":"10.1145\/1806799.1806833"},{"issue":"7","key":"21_CR26","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/s00236-017-0294-5","volume":"54","author":"S Jha","year":"2017","unstructured":"Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. Acta Informatica 54(7), 693\u2013726 (2017)","journal-title":"Acta Informatica"},{"key":"21_CR27","doi-asserted-by":"publisher","unstructured":"Kiriansky, V., Lebedev, I., Amarasinghe, S., Devadas, S., Emer, J.: Dawg: a defense against cache timing attacks in speculative execution processors. In: Proceedings of the 51st Annual IEEE\/ACM International Symposium on Microarchitecture. MICRO-51, pp. 974\u2013987. IEEE Press (2018). https:\/\/doi.org\/10.1109\/MICRO.2018.00083","DOI":"10.1109\/MICRO.2018.00083"},{"key":"21_CR28","unstructured":"Lattner, et. al.: CIRCT: Circuit IR Compilers and Tools (2025). https:\/\/circt.llvm.org\/, https:\/\/github.com\/llvm\/circt"},{"key":"21_CR29","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-030-81688-9_22","volume-title":"CAV 2021","author":"M Mann","year":"2021","unstructured":"Mann, M., et al.: Pono: a flexible and extensible SMT-based model checker. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12760, pp. 461\u2013474. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22"},{"key":"21_CR30","unstructured":"Michael Popoloski: slang (2024). https:\/\/sv-lang.com\/"},{"key":"21_CR31","unstructured":"myhdl: MyHDL (2024), Webpage. https:\/\/www.cocotb.org\/, https:\/\/docs.cocotb.org\/en\/stable\/#"},{"key":"21_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/BFb0058037","volume-title":"FSTTCS 1997","author":"KS Namjoshi","year":"1997","unstructured":"Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol. 1346, pp. 284\u2013296. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0058037"},{"key":"21_CR33","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"CAV 1994","author":"JR Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68\u201380. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_44"},{"key":"21_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-319-96145-3_32","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2018","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC and Boolector 3.0. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 587\u2013595. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_32"},{"key":"21_CR35","doi-asserted-by":"publisher","unstructured":"Nigam, R., et al.: Predictable accelerator design with time-sensitive affine types. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2020, pp. 393\u2013407. Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3385412.3385974","DOI":"10.1145\/3385412.3385974"},{"key":"21_CR36","doi-asserted-by":"publisher","unstructured":"Padon, O., Wilcox, J.R., Koenig, J.R., McMillan, K.L., Aiken, A.: Induction duality: primal-dual search for invariants. Proc. ACM Program. Lang. 6(POPL) (2022). https:\/\/doi.org\/10.1145\/3498712","DOI":"10.1145\/3498712"},{"key":"21_CR37","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems - Conference proceedings, Colle-sur-Loup (near Nice), France, 8\u201319 October 1984. NATO ASI Series, vol.\u00a013, pp. 123\u2013144. Springer, Cham (1984). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_5","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Polgreen, E., et al.: UCLID5: multi-modal formal modeling, verification, and synthesis. In: 34th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 13371, pp. 538\u2013551. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-13185-1_27"},{"key":"21_CR39","unstructured":"Polgreen, E., Reynolds, A., Seshia, S.A.: Satisfiability and synthesis modulo oracles. CoRR abs\/2107.13477 (2021). https:\/\/arxiv.org\/abs\/2107.13477"},{"key":"21_CR40","unstructured":"Semiconductor Engineering: Big Trouble at 3nm (2018). https:\/\/semiengineering.com\/big-trouble-at-3nm\/"},{"key":"21_CR41","unstructured":"Semiconductor Engineering: Verification IP (VIP) (2024). https:\/\/semiengineering.com\/knowledge_centers\/intellectual-property\/verification-ip-vip\/"},{"key":"21_CR42","doi-asserted-by":"crossref","unstructured":"Seshia, S.A.: Sciduction: combining induction, deduction, and structure for verification and synthesis. In: Proceedings of the Design Automation Conference (DAC), pp. 356\u2013365 (2012)","DOI":"10.1145\/2228360.2228425"},{"issue":"11","key":"21_CR43","doi-asserted-by":"publisher","first-page":"2036","DOI":"10.1109\/JPROC.2015.2471838","volume":"103","author":"SA Seshia","year":"2015","unstructured":"Seshia, S.A.: Combining induction, deduction, and structure for verification and synthesis. Proc. IEEE 103(11), 2036\u20132051 (2015)","journal-title":"Proc. IEEE"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Subramanyan, P.: Uclid5: integrating modeling, verification, synthesis, and learning. In: Proceedings of the 15th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) (2018)","DOI":"10.1109\/MEMCOD.2018.8556946"},{"key":"21_CR45","doi-asserted-by":"publisher","unstructured":"Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 4\u201313. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_3","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"21_CR46","doi-asserted-by":"publisher","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems. ASPLOS XII, pp. 404\u2013415. Association for Computing Machinery, New York, NY, USA (2006). https:\/\/doi.org\/10.1145\/1168857.1168907","DOI":"10.1145\/1168857.1168907"},{"key":"21_CR47","unstructured":"Synopsys: Formality Equivalence Checking (2024). https:\/\/www.synopsys.com\/implementation-and-signoff\/signoff\/formality-equivalence-checking.html"},{"key":"21_CR48","doi-asserted-by":"publisher","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352\u2013367. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11547662_24","DOI":"10.1007\/11547662_24"},{"key":"21_CR49","unstructured":"The Rocq\/Coq Development Team: Rocq Prover (2024). https:\/\/rocq-prover.org\/, https:\/\/coq.inria.fr\/"},{"key":"21_CR50","doi-asserted-by":"publisher","unstructured":"Vicarte, J.R.S., et al.: Augury: using data memory-dependent prefetchers to leak data at rest. In: 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, 22\u201326 May 2022, pp. 1491\u20131505. IEEE (2022). https:\/\/doi.org\/10.1109\/SP46214.2022.9833570","DOI":"10.1109\/SP46214.2022.9833570"},{"key":"21_CR51","doi-asserted-by":"crossref","unstructured":"Viswanathan, M., Viswanathan, R.: Foundations for circular compositional reasoning. In: Proceedings of the 28th International Colloquium on Automata, Languages and Programming. ICALP \u201901, pp. 835\u2013847. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-48224-5_68"},{"key":"21_CR52","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Gurfinkel, A.: Interpolating property directed reachability. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 260\u2013276. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_17","DOI":"10.1007\/978-3-319-08867-9_17"},{"key":"21_CR53","unstructured":"Wolf, C., Glaser, J., Kepler, J.: Yosys-A Free Verilog Synthesis Suite (2013)"},{"key":"21_CR54","unstructured":"YosysHQ: Mutation Cover with Yosys (2024). GitHub repository, https:\/\/github.com\/YosysHQ\/mcy"},{"key":"21_CR55","doi-asserted-by":"publisher","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), 30 June\u20132 July 2003, Pacific Grove, CA, USA, p.\u00a029. IEEE Computer Society (2003). https:\/\/doi.org\/10.1109\/CSFW.2003.1212703","DOI":"10.1109\/CSFW.2003.1212703"},{"key":"21_CR56","doi-asserted-by":"publisher","unstructured":"Zhang, H., Yang, W., Fedyukovich, G., Gupta, A., Malik, S.: Synthesizing environment invariants for modular hardware verification. In: Beyer, D., Zufferey, D. (eds.) VMCAI 2020. LNCS, vol. 11990, pp. 202\u2013225. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_10","DOI":"10.1007\/978-3-030-39322-9_10"}],"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-98682-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T10:31:44Z","timestamp":1783506704000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98682-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986819","9783031986826"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98682-6_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors declare that they have no interests other than their affiliations and funding sources mentioned in the acknowledgments.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}