{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:46:11Z","timestamp":1742913971495,"version":"3.40.3"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031331695"},{"type":"electronic","value":"9783031331701"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-33170-1_20","type":"book-chapter","created":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T12:55:27Z","timestamp":1685710527000},"page":"332-352","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalized High Level Synthesis with Applications to\u00a0Cryptographic Hardware"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3760-3556","authenticated-orcid":false,"given":"William","family":"Harrison","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2080-9790","authenticated-orcid":false,"given":"Ian","family":"Blumenfeld","sequence":"additional","affiliation":[]},{"given":"Eric","family":"Bond","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6277-3987","authenticated-orcid":false,"given":"Chris","family":"Hathhorn","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-0789-7410","authenticated-orcid":false,"given":"Paul","family":"Li","sequence":"additional","affiliation":[]},{"given":"May","family":"Torrence","sequence":"additional","affiliation":[]},{"given":"Jared","family":"Ziegler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,6,3]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Nowak, D., Saikawa, T.: A hierarchy of monadic effects for program verification using equational reasoning. In: Hutton, G. (ed.) Mathematics of Program Construction, pp. 226\u2013254 (2019)","DOI":"10.1007\/978-3-030-33636-3_9"},{"key":"20_CR2","unstructured":"Andrews, D.: Will the future success of reconfigurable computing require a paradigm shift in our research community\u2019s thinking?, keynote address, Applied Reconfigurable Computing (2015)"},{"key":"20_CR3","unstructured":"Armstrong, A., et al.: The state of sail. In: SpISA 2019: Workshop on Instruction Set Architecture Specification (2019)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Bachrach, J., et al.: Chisel: constructing hardware in a scala embedded language. In: DAC, pp. 1216\u20131225 (2012)","DOI":"10.1145\/2228360.2228584"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-642-03359-9_10","volume-title":"Theorem Proving in Higher Order Logics","author":"N Benton","year":"2009","unstructured":"Benton, N., Kennedy, A., Varming, C.: Some domain theory and denotational semantics in Coq. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 115\u2013130. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_10"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Claessen, K., Sheeran, M., Singh, S.: Lava: hardware design in haskell. ACM SIGPLAN Not. 34 (2001)","DOI":"10.1145\/291251.289440"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Bourgeat, T., Pit-Claudel, C., Chlipala, A.A.: The essence of Bluespec: a core language for rule-based hardware design. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 243\u2013257. PLDI 2020 (2020)","DOI":"10.1145\/3385412.3385965"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Bourke, T., Brun, L., Pouzet, M.: Mechanized semantics and verified compilation for a dataflow synchronous language with reset. Proc. ACM Program. Lang. 4(POPL) (2019)","DOI":"10.1145\/3373108"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Computer Aided Verification, pp. 24\u201340 (2010)","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Breitner, J., Spector-Zabusky, A., Li, Y., Rizkallah, C., Wiegley, J., Weirich, S.: Ready, set, verify! applying hs-to-coq to real-world haskell code (experience report). Proc. ACM Program. Lang. (2018)","DOI":"10.1145\/3236784"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Choi, J., Vijayaraghavan, M., Sherman, B., Chlipala, A.A.: Kami: a platform for high-level parametric hardware specification and its modular verification. PACMPL 1, 24:1\u201324:30 (2017)","DOI":"10.1145\/3110268"},{"key":"20_CR12","unstructured":"Model Validation Codebase. https:\/\/www.dropbox.com\/s\/r59xg34qzh0arri\/codebase_paper4262.tar.gz?dl=0 (2022)"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Du, Z., Herklotz, Y., Ramanathan, N., Wickerson, J.: Fuzzing high-level synthesis tools. In: The 2021 ACM\/SIGDA International Symposium on Field-Programmable Gate Arrays, FPGA 2021, p. 148. Association for Computing Machinery, New York (2021)","DOI":"10.1145\/3431920.3439466"},{"key":"20_CR14","unstructured":"Flor, J.P.P., Swierstra, W., Sijsling, Y.: $$\\Pi $$-Ware: hardware description and verification in agda. In: Proceedings of TYPES (2015)"},{"key":"20_CR15","doi-asserted-by":"publisher","unstructured":"Gerards, M., Baaij, C., Kuper, J., Kooijman, M.: Higher-order abstraction in hardware descriptions with C$$\\lambda $$aSH. In: Proceedings of the 2011 14th EUROMICRO Conference on Digital System Design, DSD 2011, pp. 495\u2013502. IEEE Computer Society, Washington, DC (2011). https:\/\/doi.org\/10.1109\/DSD.2011.69","DOI":"10.1109\/DSD.2011.69"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Gibbons, J., Hinze, R.: Just do it: Simple monadic equational reasoning. In: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, pp. 2\u201314 (2011)","DOI":"10.1145\/2034773.2034777"},{"issue":"1","key":"20_CR17","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.entcs.2005.01.030","volume":"132","author":"B Goldberg","year":"2005","unstructured":"Goldberg, B., Zuck, L., Barrett, C.: Into the loops: Practical issues in translation validation for optimizing compilers. Electron. Notes Theor. Comput. Sci. 132(1), 53\u201371 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Goncharov, S., Schr\u00f6der, L.: A coinductive calculus for asynchronous side-effecting processes. In: Proceedings of the 18th International Conference on Fundamentals of Computation Theory, pp. 276\u2013287 (2011)","DOI":"10.1007\/978-3-642-22953-4_24"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Gordon, M.J.C.: The semantic challenge of Verilog HDL. In: Proceedings of 10th Annual IEEE LICS, pp. 136\u2013145 (1995)","DOI":"10.1109\/LICS.1995.523251"},{"issue":"1","key":"20_CR20","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1093\/comjnl\/45.1.27","volume":"45","author":"MJC Gordon","year":"2002","unstructured":"Gordon, M.J.C.: Relating event and trace semantics of hardware description languages. Comput. J. 45(1), 27\u201336 (2002)","journal-title":"Comput. J."},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Harrison, W.L., Allwein, G.: Verifiable security templates for hardware. In: Proceedings of the Design, Automation, and Test Europe (DATE) Conference (2020)","DOI":"10.23919\/DATE48585.2020.9116342"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Harrison, W.L., Hathhorn, C., Allwein, G.: A mechanized semantic metalanguage for high level synthesis. In: 23rd International Symposium on Principles and Practice of Declarative Programming (PPDP 2021) (2021)","DOI":"10.1145\/3479394.3479417"},{"key":"20_CR23","unstructured":"Herklotz, Y., Wickerson, J.: High-level synthesis tools should be proven correct. In: Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE) (2021)"},{"key":"20_CR24","unstructured":"Huffman, B.: HOLCF 2011: A Definitional Domain Theory for Verifying Functional Programs. Ph.D. thesis, Portland State University (2012)"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Huffman, B.: Formal verification of monad transformers. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012, pp. 15\u201316 (2012)","DOI":"10.1145\/2364527.2364532"},{"key":"20_CR26","volume-title":"Contemporary Logic Design","author":"RH Katz","year":"2000","unstructured":"Katz, R.H.: Contemporary Logic Design, 2nd edn. Addison-Wesley Longman Publishing Co. Inc., Boston (2000)","edition":"2"},{"key":"20_CR27","unstructured":"Khan, W., Tiu, A., Sanan, D.: Veriformal: an executable formal model of a hardware description language. In: Roychoudhury, A., Liu, Y. (eds.) A Systems Approach to Cyber Security: Proceedings of the 2nd Singapore Cyber-Security R &D Conference (SG-CRC 2017), pp. 19\u201336. IOS Press (2017)"},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"Kloos, C., Breuer, P. (eds.): Formal Semantics for VHDL. Kluwer Academic Publishers (1995)","DOI":"10.1007\/978-1-4615-2237-9"},{"key":"20_CR29","doi-asserted-by":"publisher","unstructured":"Kundu, S., Lerner, S., Gupta, R.K.: Translation Validation of High-Level Synthesis, pp. 97\u2013121. Springer, New York (2011). https:\/\/doi.org\/10.1007\/978-1-4419-9359-5_7","DOI":"10.1007\/978-1-4419-9359-5_7"},{"issue":"7","key":"20_CR30","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"L\u00f6\u00f6w, A.: Lutsig: a verified verilog compiler for verified circuit development. In: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, pp. 46\u201360. Association for Computing Machinery, New York (2021)","DOI":"10.1145\/3437992.3439916"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"L\u00f6\u00f6w, A., Myreen, M.O.: A proof-producing translator for verilog development in HOL. In: 2019 IEEE\/ACM 7th International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 99\u2013108 (2019)","DOI":"10.1109\/FormaliSE.2019.00020"},{"key":"20_CR33","doi-asserted-by":"crossref","unstructured":"Maillard, K., et al.: Dijkstra monads for all. Proc. ACM Program. Lang. 3(ICFP) (2019)","DOI":"10.1145\/3341708"},{"key":"20_CR34","doi-asserted-by":"publisher","unstructured":"Marlow, S., Brandy, L., Coens, J., Purdy, J.: There is no fork: an abstraction for efficient, concurrent, and concise data access. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, pp. 325\u2013337. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2628136.2628144","DOI":"10.1145\/2628136.2628144"},{"issue":"5","key":"20_CR35","doi-asserted-by":"publisher","first-page":"1045","DOI":"10.1002\/j.1538-7305.1955.tb03788.x","volume":"34","author":"GH Mealy","year":"1955","unstructured":"Mealy, G.H.: A method for synthesizing sequential circuits. Bell Syst. Techn. J. 34(5), 1045\u20131079 (1955)","journal-title":"Bell Syst. Techn. J."},{"key":"20_CR36","doi-asserted-by":"crossref","unstructured":"Meredith, P., Katelman, M., Meseguer, J., Ro\u015fu, G.: A formal executable semantics of Verilog. In: Eighth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), pp. 179\u2013188 (2010)","DOI":"10.1109\/MEMCOD.2010.5558634"},{"issue":"1","key":"20_CR37","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"20_CR38","doi-asserted-by":"crossref","unstructured":"Morris, F.L.: Advice on structuring compilers and proving them correct. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1973, pp. 144\u2013152. Association for Computing Machinery, New York (1973)","DOI":"10.1145\/512927.512941"},{"key":"20_CR39","unstructured":"Mu, S.C.: Calculating a backtracking algorithm: an exercise in monadic program derivation. Technical Report, TR-IIS-19-003, Institute of Information Science, Academia Sinica (June 2019)"},{"key":"20_CR40","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, pp. 83\u201394 (2000)","DOI":"10.1145\/349299.349314"},{"key":"20_CR41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"2010","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-662-03811-6"},{"key":"20_CR42","doi-asserted-by":"crossref","unstructured":"Nienhuis, K., et al.: Rigorous engineering for hardware security: formal modelling and proof in the CHERI design and implementation process. In: 2020 IEEE Symposium on Security and Privacy, pp. 1003\u20131020 (2020)","DOI":"10.1109\/SP40000.2020.00055"},{"key":"20_CR43","unstructured":"Papaspyrou, N.S.: A resumption monad transformer and its applications in the semantics of concurrency. In: Proceedings of the 3rd Panhellenic Logic Symposium (2001). expanded version available as a tech. report from the author by request"},{"key":"20_CR44","unstructured":"Perez, I., Goodloe, A.: Copilot 3. Technical Report. 20200003164, National Aeronautics and Space Administration (NASA) (2020)"},{"key":"20_CR45","doi-asserted-by":"publisher","unstructured":"Pir\u00f3g, M., Gibbons, J.: The coinductive resumption monad. Electron. Notes Theor. Comput. Sci. 308, 273 \u2013 288 (2014). https:\/\/doi.org\/10.1016\/j.entcs.2014.10.015, http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066114000826","DOI":"10.1016\/j.entcs.2014.10.015"},{"key":"20_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151\u2013166. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054170"},{"key":"20_CR47","unstructured":"Procter, A.: Semantics-Driven Design and Implementation of High-Assurance Hardware. Ph.D. thesis, University of Missouri (2014)"},{"key":"20_CR48","doi-asserted-by":"crossref","unstructured":"Procter, A., Harrison, W., Graves, I., Becchi, M., Allwein, G.: A principled approach to secure multi-core processor design with ReWire. ACM TECS 16(2), 33:1\u201333:25 (2017)","DOI":"10.1145\/2967497"},{"key":"20_CR49","doi-asserted-by":"publisher","unstructured":"Ramanathan, N., Constantinides, G.A., Wickerson, J.: Concurrency-aware thread scheduling for high-level synthesis. In: 2018 IEEE 26th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM), pp. 101\u2013108 (2018). https:\/\/doi.org\/10.1109\/FCCM.2018.00025","DOI":"10.1109\/FCCM.2018.00025"},{"key":"20_CR50","doi-asserted-by":"publisher","unstructured":"Ramanathan, N., Fleming, S.T., Wickerson, J., Constantinides, G.A.: Hardware synthesis of weakly consistent C concurrency. In: Proceedings of the 2017 ACM\/SIGDA International Symposium on Field-Programmable Gate Arrays, FPGA 2017, pp. 169\u2013178. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3020078.3021733","DOI":"10.1145\/3020078.3021733"},{"key":"20_CR51","doi-asserted-by":"publisher","unstructured":"Reid, A.: Trustworthy specifications of ARM\u00aev8-a and v8-m system level architecture. In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp. 161\u2013168 (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886675","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"20_CR52","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of the ACM Annual Conference, vol. 2, pp. 717\u2013740. ACM (1972)","DOI":"10.1145\/800194.805852"},{"key":"20_CR53","doi-asserted-by":"crossref","unstructured":"Reynolds, T.N., Procter, A., Harrison, W., Allwein, G.: The mechanized marriage of effects and monads with applications to high-assurance hardware. ACM TECS 18(1), 6:1\u20136:26 (2019)","DOI":"10.1145\/3274282"},{"key":"20_CR54","doi-asserted-by":"crossref","unstructured":"Schr\u00f6der, L.: Bootstrapping inductive and coinductive types in hascasl. Log. Methods Comput. Sci. 4(4:17), 1\u201327 (2008)","DOI":"10.2168\/LMCS-4(4:17)2008"},{"key":"20_CR55","doi-asserted-by":"crossref","unstructured":"Sheeran, M.: muFP, a language for VLSI design. In: LISP and Functional Programming, pp. 104\u2013112 (1984)","DOI":"10.1145\/800055.802026"},{"key":"20_CR56","doi-asserted-by":"publisher","unstructured":"Singh, S., Greaves, D.J.: Kiwi: synthesis of FPGA circuits from parallel programs. In: 2008 16th International Symposium on Field-Programmable Custom Computing Machines, pp. 3\u201312 (2008). https:\/\/doi.org\/10.1109\/FCCM.2008.46","DOI":"10.1109\/FCCM.2008.46"},{"key":"20_CR57","doi-asserted-by":"publisher","unstructured":"Swierstra, W., Altenkirch, T.: Beauty in the beast. In: Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop, Haskell 2007, pp. 25\u201336. ACM, New York (2007). https:\/\/doi.org\/10.1145\/1291201.1291206","DOI":"10.1145\/1291201.1291206"},{"key":"20_CR58","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5123-2","volume-title":"Formal Semantics and Proof Techniques for Optimizing VHDL Models","author":"K Umamageswaran","year":"1999","unstructured":"Umamageswaran, K., Pandey, S.L., Wilsey, P.A.: Formal Semantics and Proof Techniques for Optimizing VHDL Models. Kluwer Academic Publishers, Boston (1999)"},{"key":"20_CR59","unstructured":"Wolf, C.: Yosys Open SYnthesis Suite. https:\/\/yosyshq.net\/yosys\/"},{"key":"20_CR60","doi-asserted-by":"publisher","unstructured":"Zeng, Y., Gupta, A., Malik, S.: Automatic generation of architecture-level models from RTL designs for processors and accelerators. In: Design, Automation & Test in Europe (DATE), pp. 460\u2013465 (2022). https:\/\/doi.org\/10.23919\/DATE54114.2022.9774527","DOI":"10.23919\/DATE54114.2022.9774527"},{"key":"20_CR61","doi-asserted-by":"crossref","unstructured":"Zeng, Y., Huang, B.Y., Zhang, H., Gupta, A., Malik, S.: Generating architecture-level abstractions from RTL designs for processors and accelerators part i: Determining architectural state variables. In: 2021 IEEE\/ACM International Conference On Computer Aided Design (ICCAD), pp. 1\u20139 (2021)","DOI":"10.1109\/ICCAD51958.2021.9643584"},{"key":"20_CR62","doi-asserted-by":"crossref","unstructured":"Zhang, B., Cheng, Z., Pedram, M.: A high-performance low-power barrett modular multiplier for cryptosystems. In: 2021 IEEE\/ACM International Symposium on Low Power Electronics and Design (ISLPED), pp. 1\u20136 (2021)","DOI":"10.1109\/ISLPED52811.2021.9502490"},{"key":"20_CR63","doi-asserted-by":"crossref","unstructured":"Zhu, H., He, J., Bowen, J.: From algebraic semantics to denotational semantics for Verilog. In: 11th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2006), p. 341\u2013360 (2006)","DOI":"10.1007\/s11334-008-0069-9"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-33170-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,21]],"date-time":"2024-10-21T18:30:15Z","timestamp":1729535415000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-33170-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031331695","9783031331701"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-33170-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"3 June 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Houston, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","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":"16 May 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/nfm-2023","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"75","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":"26","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":"3","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":"35% - 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.9","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":"6","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)"}}]}}