{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:21:18Z","timestamp":1779074478451,"version":"3.51.4"},"publisher-location":"Cham","reference-count":57,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031661488","type":"print"},{"value":"9783031661495","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-66149-5_2","type":"book-chapter","created":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:01:54Z","timestamp":1728716514000},"page":"26-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["MoXI: An Intermediate Language for\u00a0Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Kristin Yvonne","family":"Rozier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rohit","family":"Dureja","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmed","family":"Irfan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chris","family":"Johannsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karthik","family":"Nukala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,13]]},"reference":[{"key":"2_CR1","unstructured":"Biere, A.: The AIGER and-inverter graph (AIG) format version 20071012. http:\/\/fmv.jku.at\/aiger\/FORMAT. Accessed 25 July 2016"},{"key":"2_CR2","unstructured":"Biere, A.: AIGER 1.9 and beyond. http:\/\/fmv.jku.at\/hwmcc11\/beyond1.pdf. Accessed 25 July 2016"},{"key":"2_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Beer, I., Ben-David, S., Eisner, C., Landver, A.: RuleBase: an industry-oriented formal verification tool. In: Design Automation Conference, pp. 655\u2013660. IEEE (1996)","DOI":"10.1109\/DAC.1996.545656"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (eds) Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1999. LNCS, vol. 1579. Springer, Berlin, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"2_CR6","unstructured":"Biere, A., Froleyks, N., Preiner, M.: Hardware model checking competition (HWMCC) (2020). https:\/\/fmv.jku.at\/hwmcc20\/index.html"},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-319-21690-4_36","volume-title":"Computer Aided Verification","author":"M Bozzano","year":"2015","unstructured":"Bozzano, M., et al.: Formal design and safety analysis of AIR6110 wheel brake system. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification, pp. 518\u2013535. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_36"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-04468-7_15","volume-title":"Computer Safety, Reliability, and Security","author":"M Bozzano","year":"2009","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS approach: correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) Computer Safety, Reliability, and Security, pp. 173\u2013186. Springer, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04468-7_15"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: VMCAI, pp. 70\u201387 (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification, pp. 24\u201340. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: LUSTRE: a declarative language for programming synchronous systems. In: Proceedings 14th Annual ACM Symposium on Principles of Programming Languages, pp. 178\u2013188 (1987)","DOI":"10.1145\/41625.41641"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Cavada, R. et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) Proceedings 26th International Conference on Computer Aided Verification, CAV 2014. Lecture Notes in Computer Science, vol.\u00a08559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"2_CR13","unstructured":"Choi, Y., Heimdahl, M.: Model checking software requirement specifications using domain reduction abstraction. In: IEEE ASE, pp. 314\u2013317 (2003)"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Cimatti, A. et al.: NuSMV 2: an opensource tool for symbolic model checking. In: CAV 2002, Proceedings 14th International Conference. LNCS, vol. 2404, pp. 359\u2013364. Springer, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014. Proceedings 20, pp. 46\u201361. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_4","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: TACAS, pp. 93\u2013107 (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Cola\u00e7o, J.L., Pagano, B., Pouzet, M.: Scade 6: a formal language for embedded critical software development. In: 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 1\u201311. IEEE (2017)","DOI":"10.1109\/TASE.2017.8285623"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-030-39322-9_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Courant","year":"2020","unstructured":"Courant, N., S\u00e9r\u00e9, A., Shankar, N.: The correctness of a code generator for a functional language. In: Beyer, D., Zufferey, D. (eds.) VMCAI 2020. LNCS, vol. 11990, pp. 68\u201389. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_4"},{"key":"2_CR19","unstructured":"Simulink Documentation: Simulation and model-based design (2020). https:\/\/www.mathworks.com\/products\/simulink.html"},{"key":"2_CR20","unstructured":"SCADE Documentation: Ansys SCADE suite (2023). https:\/\/www.ansys.com\/products\/embedded-software\/ansys-scade-suite"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Dureja, R., Rozier, E.W.D., Rozier, K.Y.: A case study in safety, security, and availability of wireless-enabled aircraft communication networks. In: Proceedings of the 17th AIAA Aviation Technology, Integration, and Operations Conference (AVIATION). American Institute of Aeronautics and Astronautics (2017). https:\/\/doi.org\/10.2514\/6.2017-3112","DOI":"10.2514\/6.2017-3112"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Dureja, R., Rozier, K.Y.: FuseIC3: an algorithm for checking large design spaces. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD). IEEE\/ACM, Vienna, Austria (2017)","DOI":"10.23919\/FMCAD.2017.8102255"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: International Conference on Computer Aided Verification, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"2_CR24","unstructured":"Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: FMCAD, pp. 125\u2013134 (2011)"},{"issue":"4","key":"2_CR25","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theoret. Comput. Sci. 89(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"2_CR26","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-319-40648-0_12","volume-title":"NASA Formal Methods","author":"G F\u00e9rey","year":"2016","unstructured":"F\u00e9rey, G., Shankar, N.: Code generation using a formal model of reference counting. In: Rayadurgam, S., Tkachuk, O. (eds.) NASA Formal Methods, pp. 150\u2013165. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_12"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Gan, X., Dubrovin, J., Heljanko, K.: A symbolic model checking approach to verifying satellite onboard software. Sci. Comput. Program. 82, 44\u201355 (2013). http:\/\/dx.doi.org\/10.1016\/j.scico.2013.03.005","DOI":"10.1016\/j.scico.2013.03.005"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41540-6_1","volume-title":"Computer Aided Verification","author":"M Gario","year":"2016","unstructured":"Gario, M., Cimatti, A., Mattarei, C., Tonetta, S., Rozier, K.Y.: Model checking at scale: automated air traffic control design space exploration. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 3\u201322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_1"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Goel, A., Sakallah, K.: Model checking of Verilog RTL using IC3 with syntax-guided abstraction. In: NASA Formal Methods: 11th International Symposium, NFM 2019, Houston, TX, USA, May 7\u20139, 2019, Proceedings 11, pp. 166\u2013185. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9","DOI":"10.1007\/978-3-030-20652-9_11"},{"key":"2_CR30","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","author":"A Goel","year":"2020","unstructured":"Goel, A., Sakallah, K.: AVR: abstractly verifying reachability. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 413\u2013422. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_23"},{"key":"2_CR31","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/3-540-45732-1_27","volume-title":"Computer Safety, Reliability and Security","author":"M Gribaudo","year":"2002","unstructured":"Gribaudo, M., Horv\u00e1th, A., Bobbio, A., Tronci, E., Ciancamerla, E., Minichino, M.: Model-checking based on fluid petri nets for the temperature control system of the ICARO co-generative plant. In: Anderson, S., Felici, M., Bologna, S. (eds.) Computer Safety, Reliability and Security, pp. 273\u2013283. Springer, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45732-1_27"},{"key":"2_CR32","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley (2003)"},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"IEEE: IEEE standard multivalue logic system for VHDL model interoperability (Std_logic_1164) In: IEEE Std 1164-1993, pp. 1\u201324 (1993). https:\/\/doi.org\/10.1109\/IEEESTD.1993.115571","DOI":"10.1109\/IEEESTD.1993.115571"},{"key":"2_CR34","unstructured":"IEEE: IEEE standard for Verilog hardware description language (2005)"},{"key":"2_CR35","unstructured":"IEEE: IEEE standard for VHDL language reference manual (2019)"},{"key":"2_CR36","volume-title":"The LUSTRE V6 Reference Manual","author":"E Jahier","year":"2016","unstructured":"Jahier, E., Raymond, P., Halbwachs, N.: The LUSTRE V6 Reference Manual. Verimag, Grenoble (2016)"},{"key":"2_CR37","unstructured":"Johannsen, C., et al.: Symbolic model-checking intermediate-language tool suite. In: Proceedings of 36th International Conference on Computer Aided Verification (CAV). LNCS, Springer (2024)"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Lahtinen, J., Valkonen, J., Bj\u00f6rkman, K., Frits, J., Niemel\u00e4, I., Heljanko, K.: Model checking of safety-critical software in the nuclear engineering domain. Reliab. Eng. Syst. Saf. 105, 104\u2013113 (2012). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0951832012000555","DOI":"10.1016\/j.ress.2012.03.021"},{"key":"2_CR39","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)"},{"key":"2_CR40","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-030-81688-9_22","volume-title":"Computer Aided Verification","author":"M Mann","year":"2021","unstructured":"Mann, M., et al.: Pono: a flexible and extensible SMT-based model checker. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification, pp. 461\u2013474. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Mattarei, C., Cimatti, A., Gario, M., Tonetta, S., Rozier, K.Y.: Comparing different functional allocations in automated air traffic control design. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2015). IEEE\/ACM, Austin, Texas, U.S.A, September 2015","DOI":"10.1109\/FMCAD.2015.7542260"},{"key":"2_CR42","unstructured":"McMillan, K.: The SMV language. Technical report, Cadence Berkeley Lab (1999)"},{"key":"2_CR43","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Miller, S.: Will this be formal? In: TPHOLs 5170, pp. 6\u201311. Springer (2008). http:\/\/dx.doi.org\/10.1007\/978-3-540-71067-7_2","DOI":"10.1007\/978-3-540-71067-7_2"},{"key":"2_CR45","doi-asserted-by":"crossref","unstructured":"Miller, S.P., Tribble, A.C., Whalen, M.W., Per, M., Heimdahl, E.: Proving the shalls. STTT 8(4\u20135), 303\u2013319 (2006)","DOI":"10.1007\/s10009-004-0173-6"},{"key":"2_CR46","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC, and Boolector 3.0. In: Proceedings 30th International Conference on Computer Aided Verification. LNCS, vol. 10981, pp. 587\u2013595. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_32","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"2_CR47","unstructured":"The nuXmv model checker (2015). available at https:\/\/nuxmv.fbk.eu\/"},{"key":"2_CR48","unstructured":"Cavada, R., et al.: NuSMV 2.4 user manual. Technical report, CMU\/ITC-IRST (2005)"},{"key":"2_CR49","unstructured":"Raimondi, F., Lomuscio, A., Sergot, M.J.: Towards model checking interpreted systems. In: FAABS 02, LNAI 2699, pp. 115\u2013125. Springer, Cham (2002). https:\/\/doi.org\/10.1145\/860575.86079"},{"key":"2_CR50","doi-asserted-by":"publisher","unstructured":"Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: 17th International Symposium on Formal Methods (FM2011). Lecture Notes in Computer Science (LNCS), vol.\u00a06664, pp. 417\u2013431. Springer, Verlag (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_31","DOI":"10.1007\/978-3-642-21437-0_31"},{"key":"2_CR51","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-319-48869-1_2","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"KY Rozier","year":"2016","unstructured":"Rozier, K.Y.: Specification: the biggest bottleneck in formal methods and autonomy. In: Blazy, S., Chechik, M. (eds.) Verified Software. Theories, Tools, and Experiments, pp. 8\u201326. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_2"},{"key":"2_CR52","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) Formal Methods in Computer-Aided Design, pp. 127\u2013144. Springer, Berlin, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8"},{"key":"2_CR53","unstructured":"SMTLib. https:\/\/smtlib.cs.uiowa.edu\/"},{"key":"2_CR54","doi-asserted-by":"crossref","unstructured":"Tribble, A., Miller, S.: Software safety analysis of a flight management system vertical navigation function-a status report. In: DASC, vol. 1, p. 1.B.1-1.1-9 (2003)","DOI":"10.1109\/DASC.2003.1245805"},{"issue":"3","key":"2_CR55","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/MS.2009.67","volume":"26","author":"J Yoo","year":"2009","unstructured":"Yoo, J., Jee, E., Cha, S.: Formal modeling and verification of safety-critical software. Softw. IEEE 26(3), 42\u201349 (2009)","journal-title":"Softw. IEEE"},{"key":"2_CR56","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Rozier, K.Y.: Formal specification and verification of a coordination protocol for an automated air traffic control system. In: Proceedings of the 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012). Electronic Communications of the EASST, vol.\u00a053, pp. 337\u2013353. European Association of Software Science and Technology (2012)","DOI":"10.1016\/j.scico.2014.04.002"},{"issue":"3","key":"2_CR57","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/j.scico.2014.04.002","volume":"96","author":"Y Zhao","year":"2014","unstructured":"Zhao, Y., Rozier, K.Y.: Formal specification and verification of a coordination protocol for an automated air traffic control system. Sci. Comput. Program. J. 96(3), 337\u2013353 (2014)","journal-title":"Sci. Comput. Program. J."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66149-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:03:32Z","timestamp":1728716612000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66149-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,13]]},"ISBN":["9783031661488","9783031661495"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66149-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,13]]},"assertion":[{"value":"13 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}