{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:01:54Z","timestamp":1742914914766,"version":"3.40.3"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030916305"},{"type":"electronic","value":"9783030916312"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91631-2_22","type":"book-chapter","created":{"date-parts":[[2021,11,18]],"date-time":"2021-11-18T21:02:24Z","timestamp":1637269344000},"page":"394-413","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Prototyping Formal Methods Tools: A Protocol Analysis Case Study"],"prefix":"10.1007","author":[{"given":"Abigail","family":"Siegel","sequence":"first","affiliation":[]},{"given":"Mia","family":"Santomauro","sequence":"additional","affiliation":[]},{"given":"Tristan","family":"Dyer","sequence":"additional","affiliation":[]},{"given":"Tim","family":"Nelson","sequence":"additional","affiliation":[]},{"given":"Shriram","family":"Krishnamurthi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,19]]},"reference":[{"key":"22_CR1","unstructured":"Abbassi, A., Day, N.A., Rayside, D.: Astra version 1.0: evaluating translations from Alloy to SMT-LIB. CoRR abs\/1906.05881 (2019). http:\/\/arxiv.org\/abs\/1906.05881"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-14295-6_11","volume-title":"Computer Aided Verification","author":"T Ball","year":"2010","unstructured":"Ball, T., Bounimova, E., Levin, V., Kumar, R., Lichtenberg, J.: The static driver verifier research platform. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 119\u2013122. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_11"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Barwise, K.J., Allwein, G. (eds.): Logical Reasoning with Diagrams. Oxford University Press (1996)","DOI":"10.1093\/oso\/9780195104271.001.0001"},{"issue":"1\u20132","key":"22_CR4","first-page":"1","volume":"1","author":"B Blanchet","year":"2016","unstructured":"Blanchet, B.: Modeling and verifying security protocols with the applied Pi calculus and ProVerif. Found. Trends Priv. Secur. 1(1\u20132), 1\u2013135 (2016)","journal-title":"Found. Trends Priv. Secur."},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Bornholt, J., Torlak, E.: Synthesizing memory models from framework sketches and litmus tests. In: Programming Language Design and Implementation (PLDI) (2017)","DOI":"10.1145\/3062341.3062353"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-319-96142-2_26","volume-title":"Computer Aided Verification","author":"A Chudnov","year":"2018","unstructured":"Chudnov, A., et al.: Continuous formal verification of Amazon s2n. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 430\u2013446. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_26"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-319-96142-2_28","volume-title":"Computer Aided Verification","author":"B Cook","year":"2018","unstructured":"Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 467\u2013486. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_28"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415\u2013418. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_37"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-54804-8_2","volume-title":"Fundamental Approaches to Software Engineering","author":"A Cunha","year":"2014","unstructured":"Cunha, A., Macedo, N., Guimar\u00e3es, T.: Target oriented relational model finding. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 17\u201331. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54804-8_2"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-319-66197-1_11","volume-title":"Software Engineering and Formal Methods","author":"N Danas","year":"2017","unstructured":"Danas, N., Nelson, T., Harrison, L., Krishnamurthi, S., Dougherty, D.J.: User studies of principled model finder output. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 168\u2013184. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_11"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-540-71209-1_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SF Doghmi","year":"2007","unstructured":"Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523\u2013537. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_41"},{"issue":"2","key":"22_CR13","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theor. 29(2), 198\u2013207 (1983). https:\/\/doi.org\/10.1109\/TIT.1983.1056650","journal-title":"IEEE Trans. Inf. Theor."},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-98938-9_8","volume-title":"Integrated Formal Methods","author":"DJ Dougherty","year":"2018","unstructured":"Dougherty, D.J., Guttman, J.D., Ramsdell, J.D.: Security protocol analysis in context: computing minimal executions using SMT and CPSA. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 130\u2013150. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98938-9_8"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-030-77543-8_7","volume-title":"Rigorous State-Based Methods","author":"T Dyer","year":"2021","unstructured":"Dyer, T., Baugh, J.: Sterling: a web-based visualizer for relational modeling languages. In: Raschke, A., M\u00e9ry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 99\u2013104. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77543-8_7"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Felleisen, M., et al.: A programmable programming language. In: Communications of the ACM (2018)","DOI":"10.1145\/3127323"},{"issue":"2","key":"22_CR17","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1017\/S0956796801004208","volume":"12","author":"RB Findler","year":"2002","unstructured":"Findler, R.B., et al.: DrScheme: a programming environment for Scheme. J. Funct. Program. 12(2), 159\u2013182 (2002)","journal-title":"J. Funct. Program."},{"key":"22_CR18","doi-asserted-by":"publisher","unstructured":"Fogel, A., et al.: A general approach to network configuration analysis. In: Networked Systems Design and Implementation, pp. 469\u2013483 (2015). https:\/\/doi.org\/10.5555\/2789770.2789803","DOI":"10.5555\/2789770.2789803"},{"key":"22_CR19","unstructured":"Ghazi, A.A.E., Taghdiri, M.: Analyzing Alloy formulas using an SMT solver: a case study. CoRR abs\/1505.00672 (2015). http:\/\/arxiv.org\/abs\/1505.00672"},{"key":"22_CR20","doi-asserted-by":"publisher","unstructured":"Guttman, J.D.: Fair exchange in strand spaces. In: International Workshop on Security Issues in Concurrency, EPTCS, vol. 7, pp. 46\u201360 (2009). https:\/\/doi.org\/10.4204\/EPTCS.7.4","DOI":"10.4204\/EPTCS.7.4"},{"issue":"1\u20132","key":"22_CR21","first-page":"5","volume":"8","author":"JD Guttman","year":"1995","unstructured":"Guttman, J.D., Ramsdell, J.D., Wand, M.: VLISP: a verified implementation of Scheme. LISP Symb. Comput. 8(1\u20132), 5\u201332 (1995)","journal-title":"LISP Symb. Comput."},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-24725-8_23","volume-title":"Programming Languages and Systems","author":"JD Guttman","year":"2004","unstructured":"Guttman, J.D., Thayer, F.J., Carlson, J.A., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Trust management in strand spaces: a rely-guarantee method. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 325\u2013339. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24725-8_23"},{"key":"22_CR23","doi-asserted-by":"publisher","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis, 2nd edn. MIT Press (2012). https:\/\/doi.org\/10.5555\/2141100","DOI":"10.5555\/2141100"},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-65277-7_8","volume-title":"Progress in Cryptology \u2013 INDOCRYPT 2020","author":"N Kobeissi","year":"2020","unstructured":"Kobeissi, N., Nicolas, G., Tiwari, M.: Verifpal: cryptographic protocol analysis for the real world. In: Bhargavan, K., Oswald, E., Prabhakaran, M. (eds.) INDOCRYPT 2020. LNCS, vol. 12578, pp. 151\u2013202. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-65277-7_8"},{"key":"22_CR25","unstructured":"Liskov, M.D., Ramsdell, J.D., Guttman, J.D., Rowe, P.D.: The cryptographic protocol shapes analyzer: a manual. https:\/\/github.com\/mitre\/cpsa\/blob\/master\/doc\/cpsamanual.pdf. Accessed 6 Jun 2021"},{"issue":"3","key":"22_CR26","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0020-0190(95)00144-2","volume":"56","author":"G Lowe","year":"1995","unstructured":"Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Inf. Process. Lett. 56(3), 131\u2013133 (1995). https:\/\/doi.org\/10.1016\/0020-0190(95)00144-2","journal-title":"Inf. Process. Lett."},{"key":"22_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-662-46675-9_20","volume-title":"Fundamental Approaches to Software Engineering","author":"N Macedo","year":"2015","unstructured":"Macedo, N., Cunha, A., Guimar\u00e3es, T.: Exploring scenario exploration. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 301\u2013315. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_20"},{"key":"22_CR28","doi-asserted-by":"publisher","unstructured":"Macedo, N., Guimar\u00e3es, T., Cunha, A.: Model repair and transformation with Echo. In: Automated Software Engineering (2013). https:\/\/doi.org\/10.1109\/ASE.2013.6693135","DOI":"10.1109\/ASE.2013.6693135"},{"key":"22_CR29","doi-asserted-by":"publisher","unstructured":"Marinov, D., Khurshid, S.: TestEra: a novel framework for automated testing of Java programs. In: Automated Software Engineering (2001). https:\/\/doi.org\/10.1109\/ASE.2001.989787","DOI":"10.1109\/ASE.2001.989787"},{"key":"22_CR30","unstructured":"McCormick, K.D., Cinelli, F.C.: Translating Alloy to SMT-LIB. Major qualifying project (b.s. thesis), Worcester Polytechnic Institute (2018)"},{"key":"22_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-63046-5_10","volume-title":"Automated Deduction \u2013 CADE 26","author":"B Meng","year":"2017","unstructured":"Meng, B., Reynolds, A., Tinelli, C., Barrett, C.: Relational constraint solving in SMT. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 148\u2013165. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_10"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Misailovic, S., Marinov, D., Khurshid, S.: Korat: a tool for generating structurally complex test inputs. In: International Conference on Software Engineering (2007)","DOI":"10.1109\/ICSE.2007.48"},{"key":"22_CR33","doi-asserted-by":"crossref","unstructured":"Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: International Conference on Software Engineering (2015)","DOI":"10.1109\/ICSE.2015.77"},{"key":"22_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-662-54494-5_2","volume-title":"Fundamental Approaches to Software Engineering","author":"V Montaghami","year":"2017","unstructured":"Montaghami, V., Rayside, D.: Bordeaux: a tool for thinking outside the box. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 22\u201339. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54494-5_2"},{"issue":"12","key":"22_CR35","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"RM Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978). https:\/\/doi.org\/10.1145\/359657.359659","journal-title":"Commun. ACM"},{"key":"22_CR36","unstructured":"Nelson, T., Ferguson, A.D., Scheer, M.J.G., Krishnamurthi, S.: Tierless programming and reasoning for software-defined networks. In: Networked Systems Design and Implementation (2014)"},{"key":"22_CR37","doi-asserted-by":"crossref","unstructured":"Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: International Conference on Software Engineering (2013)","DOI":"10.1109\/ICSE.2013.6606569"},{"key":"22_CR38","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: USENIX Large Installation System Administration Conference (2010)"},{"key":"22_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-30885-7_10","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"T Nelson","year":"2012","unstructured":"Nelson, T., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Toward a more complete Alloy. In: Derrick, J., et al. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 136\u2013149. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30885-7_10"},{"key":"22_CR40","unstructured":"Neumerkel, U., Kral, S.: Declarative program development in prolog with GUPU. In: International Workshop on Logic Programming Environments, pp. 77\u201386 (2002)"},{"issue":"4","key":"22_CR41","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/2699417","volume":"58","author":"C Newcombe","year":"2015","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How AWS uses formal methods. Commun. ACM 58(4), 66\u201373 (2015). https:\/\/doi.org\/10.1145\/2699417","journal-title":"Commun. ACM"},{"key":"22_CR42","doi-asserted-by":"crossref","unstructured":"Porncharoenwase, S., Nelson, T., Krishnamurthi, S.: CompoSAT: specification-guided coverage for model finding. In: International Symposium on Formal Methods (FM) (2018)","DOI":"10.1007\/978-3-319-95582-7_34"},{"key":"22_CR43","unstructured":"Ptolemaeus, C. (ed.): System design, modeling, and simulation using Ptolemy II. Ptolemy.org (2014). http:\/\/ptolemy.org\/books\/Systems"},{"key":"22_CR44","doi-asserted-by":"publisher","unstructured":"Rupakheti, C.R., Hou, D.: An abstraction-oriented, path-based approach for analyzing object equality in Java. In: Working Conference on Reverse Engineering (2010). https:\/\/doi.org\/10.1109\/WCRE.2010.30","DOI":"10.1109\/WCRE.2010.30"},{"key":"22_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-319-21401-6_30","volume-title":"Automated Deduction - CADE-25","author":"S Saghafi","year":"2015","unstructured":"Saghafi, S., Danas, N., Dougherty, D.J.: Exploring theories with a model-finding assistant. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 434\u2013449. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_30"},{"key":"22_CR46","unstructured":"Sergey Bronnikov: Practical FM. https:\/\/github.com\/ligurio\/practical-fm. Accessed 23 Jan 2021"},{"key":"22_CR47","unstructured":"Shimojima, A.: On the Efficacy of Representation. Ph.D. thesis. The Department of Philosophy, Indiana University (1996)"},{"key":"22_CR48","doi-asserted-by":"publisher","unstructured":"Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for Alloy. In: Software Testing, Verification and Validation (ICST) (2017). https:\/\/doi.org\/10.1109\/ICST.2017.31","DOI":"10.1109\/ICST.2017.31"},{"key":"22_CR49","doi-asserted-by":"publisher","unstructured":"Sullivan, A., Zaeem, R.N., Khurshid, S., Marinov, D.: Towards a test automation framework for Alloy. In: Symposium on Model Checking of Software (SPIN). pp. 113\u2013116 (2014). https:\/\/doi.org\/10.1145\/2632362.2632369","DOI":"10.1145\/2632362.2632369"},{"key":"22_CR50","unstructured":"Tariq, Khadija: Linking Alloy with SMT-based Finite Model Finding. Master\u2019s thesis, University of Waterloo (2021). http:\/\/hdl.handle.net\/10012\/16756"},{"issue":"1","key":"22_CR51","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"FJ Thayer","year":"1999","unstructured":"Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. J. Comput. Secur. 7(1), 191\u2013230 (1999)","journal-title":"J. Comput. Secur."},{"key":"22_CR52","doi-asserted-by":"crossref","unstructured":"Torlak, E., Bodik, R.: Growing solver-aided languages with Rosette. In: Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software. SPLASH Onward! (2013)","DOI":"10.1145\/2509578.2509586"},{"key":"22_CR53","doi-asserted-by":"crossref","unstructured":"Torlak, E., Bodik, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: Programming Language Design and Implementation (PLDI) (2014)","DOI":"10.1145\/2594291.2594340"},{"key":"22_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_49"}],"container-title":["Lecture Notes in Computer Science","Protocols, Strands, and Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91631-2_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,9]],"date-time":"2022-05-09T13:07:18Z","timestamp":1652101638000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91631-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030916305","9783030916312"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91631-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"19 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}