乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T21:40:01Z","timestamp":1732484401978,"version":"3.28.0"},"publisher-location":"Cham","reference-count":65,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656262"},{"type":"electronic","value":"9783031656279"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"Abstract<\/jats:title>We release the first tool suite implementingMoXI<\/jats:sc>(Model eXchange Interlingua), an intermediate language for symbolic model checking designed to be an international research-community standard and developed by a widespread collaboration under a National Science Foundation (NSF) CISE Community Research Infrastructure initiative. Although we focus here on hardware verification, theMoXI<\/jats:sc>language is useful for software model checking and verification of infinite-state systems in general.MoXI<\/jats:sc>builds on elements of SMT-LIB 2; it is easy to add new theories and operators. Our contributions include: (1) introducing the first tool suite of automated translators into and out of the new model-checking intermediate language; (2) composing an initial example benchmark set enabling the model-checking research community to build future translations; (3) compiling details for utilizing, extending, and improving upon our tool suite, including usage characteristics and initial performance data. Experimental evaluations demonstrate that compiling SMV-language models throughMoXI<\/jats:sc>to perform symbolic model checking with the tools from the last Hardware Model Checking Competition performs competitively with model checking directly vianuXmv<\/jats:sc>.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_10","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"203-218","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["The MoXI Model Exchange Tool Suite"],"prefix":"10.1007","author":[{"given":"Chris","family":"Johannsen","sequence":"first","affiliation":[]},{"given":"Karthik","family":"Nukala","sequence":"additional","affiliation":[]},{"given":"Rohit","family":"Dureja","sequence":"additional","affiliation":[]},{"given":"Ahmed","family":"Irfan","sequence":"additional","affiliation":[]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]},{"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"10_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-031-57256-2_7","volume-title":"TACAS 2024","author":"Z \u00c1d\u00e1m","year":"2024","unstructured":"\u00c1d\u00e1m, Z., Beyer, D., Chien, P.C., Lee, N.Z., Sirrenberg, N.: Btor2-Cert: a certifying hardware-verification framework using software analyzers. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) TACAS 2024. LNCS, vol. 14572, pp. 129\u2013149. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_7"},{"key":"10_CR2","unstructured":"The AIGER and-inverter graph (AIG) format version 20071012. http:\/\/fmv.jku.at\/aiger\/FORMAT. Accessed 25 July 2016"},{"key":"10_CR3","unstructured":"AIGER 1.9 and beyond. http:\/\/fmv.jku.at\/hwmcc11\/beyond1.pdf. Accessed 25 July 2016"},{"key":"10_CR4","unstructured":"AIGER website. http:\/\/fmv.jku.at\/aiger\/. Accessed 25 July 2016"},{"key":"10_CR5","unstructured":"Alur, R.: Principles of Cyber-physical Systems. MIT Press, Cambridge (2015)"},{"key":"10_CR6","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). https:\/\/smt-lib.org"},{"key":"10_CR7","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":"10_CR8","unstructured":"Beazley, D.: SLY (sly lex yacc) (2018). https:\/\/sly.readthedocs.io\/en\/latest\/"},{"key":"10_CR9","unstructured":"Bensalem, S., et al.: An overview of SAL. In: Holloway, C.M. (ed.) LFM 2000: Fifth NASA Langley Formal Methods Workshop, pp. 187\u2013196. NASA Langley Research Center, Hampton, June 2000. http:\/\/www.csl.sri.com\/papers\/lfm2000\/"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Beyer, D.: State of the art in software verification and witness validation: SV-COMP 2024. In: Finkbeiner, B., Kov\u00e1cs, L. (eds) TACAS 2024. LNCS, vol. 14572, pp. 299\u2013329. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_15","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"10_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-031-30820-8_12","volume-title":"TACAS 2023","author":"D Beyer","year":"2023","unstructured":"Beyer, D., Chien, P.C., Lee, N.Z.: Bridging hardware and software analysis with BTOR2C: a word-level-circuit-to-C translator. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 152\u2013172. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_12"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"10_CR13","unstructured":"Biere, A., Froleyks, N., Preiner, M.: Hardware Model Checking Competition (HWMCC) (2020). https:\/\/fmv.jku.at\/hwmcc20\/index.html"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","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.) CAV 2015. LNCS, vol. 9206, pp. 518\u2013535. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_36"},{"key":"10_CR15","unstructured":"Bozzano, M., et al.: nuXmv 1.0 User Manual. Technical report, FBK - Via Sommarive 18, 38055 Povo (Trento) - Italy (2014)"},{"key":"10_CR16","unstructured":"Bozzano, M., et al.: nuXmv 2.0. 0 user manual. Fondazione Bruno Kessler, Technical report, Trento, Italy (2019)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","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.) SAFECOMP 2009. LNCS, vol. 5775, pp. 173\u2013186. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04468-7_15"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","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.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: LUSTRE: a declarative language for programming synchronous systems. In: Proceedings of the\u00a014th Annual ACM Symposium on Principles of Programming Languages, pp. 178\u2013188 (1987)","DOI":"10.1145\/41625.41641"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"10_CR21","unstructured":"Cavada, R., et al.: NuSMV 2.6 user manual (2016)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/978-3-319-41540-6_29","volume-title":"Computer Aided Verification","author":"A Champion","year":"2016","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 510\u2013517. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29"},{"key":"10_CR23","unstructured":"Choi, Y., Heimdahl, M.: Model checking software requirement specifications using domain reduction abstraction. In: IEEE ASE, pp. 314\u2013317 (2003)"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"10_CR26","unstructured":"Cimatti, A., Griggio, A., Tonetta, S., et\u00a0al.: The VMT-LIB language and tools. In: Proceedings of the 20th Internal Workshop on Satisfiability ModuloTheories co-located with the 11th International Joint Conference on Automated Reasoning $$\\{$$(IJCAR$$\\}$$ 2022) part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, 11\u201312 August 2022, vol.\u00a03185, pp. 80\u201389. CEUR-WS. org (2022)"},{"key":"10_CR27","unstructured":"Documentation, S.: Simulation and model-based design (2020). https:\/\/www.mathworks.com\/products\/simulink.html"},{"key":"10_CR28","unstructured":"Documentation, SCADE: Ansys SCADE Suite (2023). https:\/\/www.ansys.com\/products\/embedded-software\/ansys-scade-suite"},{"key":"10_CR29","doi-asserted-by":"publisher","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, June 2017. https:\/\/doi.org\/10.2514\/6.2017-3112","DOI":"10.2514\/6.2017-3112"},{"key":"10_CR30","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), Vienna, Austria. IEEE\/ACM, October 2017","DOI":"10.23919\/FMCAD.2017.8102255"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"10_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-319-77935-5_8","volume-title":"NASA Formal Methods","author":"B Dutertre","year":"2018","unstructured":"Dutertre, B., Jovanovi\u0107, D., Navas, J.A.: Verification of fault-tolerant protocols with sally. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 113\u2013120. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-77935-5_8"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Gan, X., Dubrovin, J., Heljanko, K.: A symbolic model checking approach to verifying satellite onboard software. Sci. Comput. Programm. (2013). http:\/\/dx.doi.org\/10.1016\/j.scico.2013.03.005","DOI":"10.1016\/j.scico.2013.03.005"},{"key":"10_CR34","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":"10_CR35","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","author":"A Goel","year":"2020","unstructured":"Goel, A., Sakallah, K.: AVR: abstractly verifying reachability. In: TACAS 2020. LNCS, vol. 12078, pp. 413\u2013422. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_23"},{"key":"10_CR36","series-title":"Lecture Notes in Computer Science","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.) SAFECOMP 2002. LNCS, vol. 2434, pp. 273\u2013283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45732-1_27"},{"key":"10_CR37","unstructured":"Holzmann, G.: Design and Validation of Computer Protocols. Prentice-Hall Int, Editions (1991)"},{"key":"10_CR38","unstructured":"Hunt, W.: FMCAD organization home page. http:\/\/www.cs.utexas.edu\/users\/hunt\/FMCAD\/"},{"key":"10_CR39","unstructured":"IEEE: IEEE standard for Verilog hardware description language (2005)"},{"key":"10_CR40","unstructured":"IEEE: IEEE standard for VHDL language reference manual (2019)"},{"key":"10_CR41","unstructured":"Kessler, F.B.: Verification modulo theories. https:\/\/vmt-lib.fbk.eu\/. Accessed 30 Sept 2017"},{"key":"10_CR42","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. Safety 105(0), 104\u2013113 (2012). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0951832012000555","DOI":"10.1016\/j.ress.2012.03.021"},{"key":"10_CR43","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading (2002)"},{"key":"10_CR44","series-title":"Lecture Notes in Computer Science","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.) CAV 2021, Part II. LNCS, vol. 12760, pp. 461\u2013474. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_22"},{"key":"10_CR45","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":"10_CR46","unstructured":"McMillan, K.: The SMV language. Technical report, Cadence Berkeley Lab (1999)"},{"key":"10_CR47","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking, chap. The SMV System, pp. 61\u201385. Springer, Boston (1993). https:\/\/doi.org\/10.1007\/978-1-4615-3190-6_4","DOI":"10.1007\/978-1-4615-3190-6_4"},{"key":"10_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-540-71067-7_2","volume-title":"Theorem Proving in Higher Order Logics","author":"SP Miller","year":"2008","unstructured":"Miller, S.P.: Will this be formal? In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 6\u201311. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_2"},{"issue":"4\u20135","key":"10_CR49","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/s10009-004-0173-6","volume":"8","author":"SP Miller","year":"2006","unstructured":"Miller, S.P., Tribble, A.C., Whalen, M.W., Per, M., Heimdahl, E.: Proving the shalls. STTT 8(4\u20135), 303\u2013319 (2006)","journal-title":"Proving the shalls. STTT"},{"key":"10_CR50","unstructured":"de\u00a0Moura, L., Owre, S., Shankar, N.: The SAL language manual. CSL Technical report SRI-CSL-01-02 (Rev. 2), SRI Int\u2019l, 333 Ravenswood Ave., Menlo Park, CA 94025, August 2003"},{"key":"10_CR51","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\u00a03.0. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 587\u2013595. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_32"},{"key":"10_CR52","unstructured":"The nuXmv model checker (2015). https:\/\/nuxmv.fbk.eu\/"},{"key":"10_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"10_CR54","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-540-45133-4_10","volume-title":"Formal Approaches to Agent-Based Systems","author":"A Lomuscio","year":"2003","unstructured":"Lomuscio, A., \u0141asica, T., Penczek, W.: Bounded model checking for interpreted systems: preliminary experimental results. In: Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C., Gordon-Spears, D. (eds.) FAABS 2002. LNCS (LNAI), vol. 2699, pp. 115\u2013125. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45133-4_10"},{"key":"10_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-54862-8_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Reinbacher","year":"2014","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 357\u2013372. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_24"},{"key":"10_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-21437-0_31","volume-title":"FM 2011: Formal Methods","author":"KY Rozier","year":"2011","unstructured":"Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417\u2013431. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_31"},{"key":"10_CR57","doi-asserted-by":"crossref","unstructured":"Rozier, K.Y., et al.: MoXI: an intermediate language for symbolic model checking. In: Proceedings of the 30th International Symposium on Model Checking Software (SPIN). LNCS, Springer (2024)","DOI":"10.1007\/978-3-031-66149-5_2"},{"key":"10_CR58","unstructured":"Rozier, K.Y., Shankar, N., Tinelli, C., Vardi, M.Y.: Developing an open-source, state-of-the-art symbolic model-checking framework for the model-checking research community (2019). https:\/\/modelchecker.github.io"},{"key":"10_CR59","doi-asserted-by":"crossref","unstructured":"Schumann, J., Rozier, K.Y., Reinbacher, T., Mengshoel, O.J., Mbaya, T., Ippolito, C.: Towards real-time, on-board, hardware-supported sensor and software health management for unmanned aerial systems. In: Proceedings of the 2013 Annual Conference of the Prognostics and Health Management Society (PHM2013), pp. 381\u2013401, October 2013","DOI":"10.36001\/phmconf.2013.v5i1.2275"},{"key":"10_CR60","series-title":"Lecture Notes in Computer Science","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.) FMCAD 2000. LNCS, vol. 1954, pp. 127\u2013144. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40922-X_8"},{"key":"10_CR61","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, pp. 1.B.1\u20131.1\u20139 v1 (2003)","DOI":"10.1109\/DASC.2003.1245805"},{"key":"10_CR62","unstructured":"Wolf, C.: Yosys open synthesis suite (2016)"},{"issue":"3","key":"10_CR63","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":"10_CR64","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":"10_CR65","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. Programm. J. 96(3), 337\u2013353 (2014)","journal-title":"Sci. Comput. Programm. J."}],"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-65627-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T21:19:07Z","timestamp":1732483147000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":65,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}