{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T10:29:55Z","timestamp":1768213795091,"version":"3.49.0"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032156990","type":"print"},{"value":"9783032157003","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-15700-3_18","type":"book-chapter","created":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:21:46Z","timestamp":1768202506000},"page":"383-407","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Probabilistic Verification for\u00a0Modular Network-on-Chip Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1938-8204","authenticated-orcid":false,"given":"Nick","family":"Waddoups","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6555-005X","authenticated-orcid":false,"given":"Jonah","family":"Boe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4860-1089","authenticated-orcid":false,"given":"Prabal","family":"Basu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3927-1612","authenticated-orcid":false,"given":"Sanghamitra","family":"Roy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0228-2737","authenticated-orcid":false,"given":"Koushik","family":"Chakraborty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8269-9489","authenticated-orcid":false,"given":"Zhen","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,13]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Alhubail, L., Bagherzadeh, N.: Power and performance optimal noc design for cpu-gpu architecture using formal models. In: 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 634\u2013637 (2019). https:\/\/doi.org\/10.23919\/DATE.2019.8714769","DOI":"10.23919\/DATE.2019.8714769"},{"key":"18_CR2","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/978-3-319-10575-8_28","volume-title":"Handbook of Model Checking","author":"C Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Baier, C., D\u2019Argenio, P.R., Gr\u00f6\u00dfer, M.: Partial order reduction for probabilistic branching time. In: Cerone, A., Wiklicky, H. (eds.) Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL 2005). Electronic Notes in Theoretical Computer Science, vol.\u00a0153, pp. 97\u2013116. Elsevier (2005). https:\/\/doi.org\/10.1016\/J.ENTCS.2005.10.034","DOI":"10.1016\/J.ENTCS.2005.10.034"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Ciesinski, F.: Partial order reduction for probabilistic systems. In: 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), pp. 230\u2013239. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/QEST.2004.1348037","DOI":"10.1109\/QEST.2004.1348037"},{"issue":"7","key":"18_CR5","doi-asserted-by":"publisher","first-page":"2035","DOI":"10.1109\/TVLSI.2017.2673808","volume":"25","author":"P Basu","year":"2017","unstructured":"Basu, P., Shridevi, R.J., Chakraborty, K., Roy, S.: IcoNoClast: tackling voltage noise in the NoC power supply through flow-control and routing algorithms. IEEE Trans. VLSI Syst. 25(7), 2035\u20132044 (2017)","journal-title":"IEEE Trans. VLSI Syst."},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Becchu, N.K.R., Harishchandra, V.M., Yernad Balachandra, N.K.: System level fault-tolerance core mapping and fpga-based verification of noc. Microelectron. J. 70, 16\u201326 (2017). https:\/\/doi.org\/10.1016\/j.mejo.2017.09.010. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0026269217302884","DOI":"10.1016\/j.mejo.2017.09.010"},{"key":"18_CR7","doi-asserted-by":"publisher","unstructured":"Boe, J.W.: Probabilistic Verification for Modular Network-on-Chip Systems. Master\u2019s thesis, Utah State University (2023). https:\/\/doi.org\/10.26076\/4f5a-4a68. https:\/\/digitalcommons.usu.edu\/etd\/8763","DOI":"10.26076\/4f5a-4a68"},{"issue":"10","key":"18_CR8","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: MoDeST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812\u2013830 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.104","journal-title":"IEEE Trans. Softw. Eng."},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-319-89963-3_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2018","unstructured":"Budde, C.E., D\u2019Argenio, P.R., Hartmanns, A., Sedwards, S.: A statistical model checker for nondeterminism and rare events. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 340\u2013358. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_20"},{"issue":"10","key":"18_CR10","doi-asserted-by":"publisher","first-page":"2532","DOI":"10.1021\/acssynbio.1c00159","volume":"10","author":"L Buecherl","year":"2021","unstructured":"Buecherl, L., et al.: Stochastic hazard analysis of genetic circuits in iBioSim and STAMINA. ACS Synth. Biol. 10(10), 2532\u20132540 (2021). https:\/\/doi.org\/10.1021\/acssynbio.1c00159. pMID: 34606710","journal-title":"ACS Synth. Biol."},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: Lustre: a declarative language for real-time programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL \u201987, pp. 178\u2013188. Association for Computing Machinery, New York (1987). https:\/\/doi.org\/10.1145\/41625.41641. https:\/\/doi-org.dist.lib.usu.edu\/10.1145\/41625.41641","DOI":"10.1145\/41625.41641"},{"key":"18_CR12","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The kind 2 model checker. In: International Conference on Computer Aided Verification (2016). https:\/\/api.semanticscholar.org\/CorpusID:11582048","DOI":"10.1007\/978-3-319-41540-6_29"},{"key":"18_CR14","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Niebert, P.: Partial order reduction on concurrent probabilistic programs. In: 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), pp. 240\u2013249. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/QEST.2004.1348038","DOI":"10.1109\/QEST.2004.1348038"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Fang, L., Yamagata, Y., Oiwa, Y.: Evaluation of A resilience embedded system using probabilistic model-checking. In: Pang, J., Liu, Y. (eds.) Proceedings Third International Workshop on Engineering Safety and Security Systems, ESSS 2014, Singapore, Singapore, 13 May 2014. EPTCS, vol.\u00a0150, pp. 35\u201349 (2014). https:\/\/doi.org\/10.4204\/EPTCS.150.4","DOI":"10.4204\/EPTCS.150.4"},{"key":"18_CR16","unstructured":"Artifact repository for \u201cprobabilistic verification for modular network-on-chip systems\u201d (2025). https:\/\/github.com\/formal-verification-research\/VMCAI26_Modular_NoC_Artifact. Accessed 16 Sept 2025"},{"issue":"2","key":"18_CR17","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/S10703-012-0167-Z","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191\u2013232 (2013). https:\/\/doi.org\/10.1007\/S10703-012-0167-Z","journal-title":"Formal Methods Syst. Des."},{"key":"18_CR18","doi-asserted-by":"publisher","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22","DOI":"10.1007\/978-3-319-06410-9_22"},{"issue":"5","key":"18_CR19","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994). https:\/\/doi.org\/10.1007\/BF01211866","journal-title":"Formal Aspects Comput."},{"key":"18_CR20","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: Explicit model checking of very large MDP using partitioning and secondary storage. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings. Lecture Notes in Computer Science, vol.\u00a09364, pp. 131\u2013147. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_10","DOI":"10.1007\/978-3-319-24953-7_10"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: A modest markov automata tutorial. In: Kr\u00f6tzsch, M., Stepanova, D. (eds.) Reasoning Web. Explainable Artificial Intelligence - 15th International Summer School 2019, Bolzano, Italy, 20\u201324 September 2019, Tutorial Lectures. Lecture Notes in Computer Science, vol. 11810, pp. 250\u2013276. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-31423-1_8","DOI":"10.1007\/978-3-030-31423-1_8"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"Hensel, C., Junges, S., Katoen, J.-P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transfer 1\u201322 (2021). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","DOI":"10.1007\/s10009-021-00633-z"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Jeppson, J., et al.: STAMINA in C++: modernizing an infinite-state probabilistic model checker. In: Jansen, N., Tribastone, M. (eds.) Quantitative Evaluation of Systems - 20th International Conference, QEST 2023, Antwerp, Belgium, 20\u201322 September 2023, Proceedings. Lecture Notes in Computer Science, vol. 14287, pp. 101\u2013109. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-43835-6_7","DOI":"10.1007\/978-3-031-43835-6_7"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Jerger, N.E., Krishna, T., Peh, L.S.: On-chip networks. In: Synthesis Lectures on Computer Architecture, Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-031-01755-1","DOI":"10.1007\/978-3-031-01755-1"},{"issue":"5","key":"18_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TASC.2014.2346484","volume":"24","author":"SY Jiang","year":"2014","unstructured":"Jiang, S.Y., Luo, G., Liu, Y., Jiang, S.S., Li, X.T.: Fault-tolerant routing algorithm simulation and hardware verification of noc. IEEE Trans. Appl. Supercond. 24(5), 1\u20135 (2014). https:\/\/doi.org\/10.1109\/TASC.2014.2346484","journal-title":"IEEE Trans. Appl. Supercond."},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: 2016 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201315 (2016)","DOI":"10.1145\/2933575.2934574"},{"key":"18_CR28","doi-asserted-by":"publisher","unstructured":"Kumar, J.A., Vasudevan, S.: Automatic compositional reasoning for probabilistic model checking of hardware designs. In: QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15\u201318 September 2010, pp. 143\u2013152. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/QEST.2010.25","DOI":"10.1109\/QEST.2010.25"},{"key":"18_CR29","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"18_CR30","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic Model Checking, pp. 220\u2013270. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72522-0_6","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"18_CR31","doi-asserted-by":"publisher","unstructured":"Lakin, M., Parker, D., Cardelli, L., Kwiatkowska, M., Phillips, A.: Design and analysis of DNA strand displacement devices using probabilistic model checking. J. R. Soc. Interface 9 (2012). https:\/\/doi.org\/10.1098\/rsif.2011.0800","DOI":"10.1098\/rsif.2011.0800"},{"key":"18_CR32","doi-asserted-by":"publisher","unstructured":"Lecler, J.J., Baillieu, G.: Application driven network-on-chip architecture exploration and refinement for a complex soc. Design Autom. Emb. Sys. 15, 133\u2013158 (2011). https:\/\/doi.org\/10.1007\/s10617-011-9075-5","DOI":"10.1007\/s10617-011-9075-5"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_11"},{"key":"18_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-030-27008-7_7","volume-title":"Formal Methods for Industrial Critical Systems","author":"B Lewis","year":"2019","unstructured":"Lewis, B., Hartmanns, A., Basu, P., Jayashankara Shridevi, R., Chakraborty, K., Roy, S., Zhang, Z.: Probabilistic verification for reliable network-on-chip system design. In: Larsen, K.G., Willemse, T. (eds.) FMICS 2019. LNCS, vol. 11687, pp. 110\u2013126. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-27008-7_7"},{"key":"18_CR35","doi-asserted-by":"publisher","unstructured":"Madsen, C., Myers, C.J., Roehner, N., Winstead, C., Zhang, Z.: Utilizing stochastic model checking to analyze genetic circuits. In: 2012 IEEE Symposium on Computational Intelligence in Bioinformatics and Computational Biology (CIBCB), pp. 379\u2013386 (2012). https:\/\/doi.org\/10.1109\/CIBCB.2012.6217255","DOI":"10.1109\/CIBCB.2012.6217255"},{"key":"18_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-40349-1_5","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2013","author":"R Maes","year":"2013","unstructured":"Maes, R.: An accurate probabilistic reliability model for silicon PUFs. In: Bertoni, G., Coron, J.-S. (eds.) CHES 2013. LNCS, vol. 8086, pp. 73\u201389. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40349-1_5"},{"key":"18_CR37","doi-asserted-by":"crossref","unstructured":"Mundhenk, P., Steinhorst, S., Lukasiewycz, M., Fahmy, S.A., Chakraborty, S.: Security analysis of automotive architectures using probabilistic model checking. In: Proceedings of the 52nd Annual Design Automation Conference, p.\u00a038. ACM (2015)","DOI":"10.1145\/2744769.2744906"},{"key":"18_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-030-85248-1_16","volume-title":"Formal Methods for Industrial Critical Systems","author":"R Roberts","year":"2021","unstructured":"Roberts, R., et al.: Probabilistic verification for reliability of a two-by-two network-on-chip system. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 232\u2013248. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_16"},{"key":"18_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-030-94583-1_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Roberts","year":"2022","unstructured":"Roberts, R., Neupane, T., Buecherl, L., Myers, C.J., Zhang, Z.: STAMINA 2.0: improving scalability of\u00a0infinite-state stochastic model checking. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 319\u2013331. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_16"},{"key":"18_CR40","doi-asserted-by":"publisher","unstructured":"Royannez, P., et al.: 90 nm low leakage soc design techniques for wireless applications. In: ISSCC. 2005 IEEE International Digest of Technical Papers, Solid-State Circuits Conference, 2005, vol. 1, pp. 138\u2013589 (2005). https:\/\/doi.org\/10.1109\/ISSCC.2005.1493907","DOI":"10.1109\/ISSCC.2005.1493907"},{"issue":"11","key":"18_CR41","doi-asserted-by":"publisher","first-page":"3265","DOI":"10.1109\/TC.2016.2532871","volume":"65","author":"R Salamat","year":"2016","unstructured":"Salamat, R., Khayambashi, M., Ebrahimi, M., Bagherzadeh, N.: A resilient routing algorithm with formal reliability analysis for partially connected 3d-nocs. IEEE Trans. Comput. 65(11), 3265\u20133279 (2016). https:\/\/doi.org\/10.1109\/TC.2016.2532871","journal-title":"IEEE Trans. Comput."},{"key":"18_CR42","doi-asserted-by":"publisher","unstructured":"Sepulveda, J., Aboul-Hassan, D., Sigl, G., Becker, B., Sauer, M.: Towards the formal verification of security properties of a network-on-chip router. In: 2018 IEEE 23rd European Test Symposium (ETS), pp.\u00a01\u20136 (2018). https:\/\/doi.org\/10.1109\/ETS.2018.8400692","DOI":"10.1109\/ETS.2018.8400692"},{"key":"18_CR43","doi-asserted-by":"crossref","unstructured":"Shridevi, R.J., Ancajas, D.M., Chakraborty, K., Roy, S.: Tackling voltage emergencies in noc through timing error resilience. In: ISLPED, pp. 104\u2013109 (2015)","DOI":"10.1109\/ISLPED.2015.7273498"},{"key":"18_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"705","DOI":"10.1007\/978-3-642-31424-7_53","volume-title":"Computer Aided Verification","author":"S Song","year":"2012","unstructured":"Song, S., Sun, J., Liu, Y., Dong, J.S.: A model checker for hierarchical probabilistic real-time systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 705\u2013711. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_53"},{"key":"18_CR45","doi-asserted-by":"publisher","unstructured":"IEEE Standard for SystemVerilog\u2013Unified Hardware Design, Specification, and Verification Language (2018). https:\/\/doi.org\/10.1109\/IEEESTD.2018.8299595","DOI":"10.1109\/IEEESTD.2018.8299595"},{"key":"18_CR46","doi-asserted-by":"publisher","unstructured":"Taylor, L., Israelsen, B., Zhang, Z.: Cycle and commute: rare-event probability verification for chemical reaction networks. In: Nadel, A., Rozier, K.Y. (eds.) Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD 2023, pp. 284\u2013293. TU Wien Academic Press (2023). https:\/\/doi.org\/10.34727\/2023\/isbn.978-3-85448-060-0_37","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_37"},{"key":"18_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-030-94583-1_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Taylor","year":"2022","unstructured":"Taylor, L., Zhang, Z.: Scaling up livelock verification for network-on-chip routing algorithms. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 378\u2013399. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_19"},{"key":"18_CR48","doi-asserted-by":"publisher","unstructured":"Tsai, L., Hu, C.: Networks on chips: structure and design methodologies. J. Electric. Comput. Eng. 2012 (2012). https:\/\/doi.org\/10.1155\/2012\/509465","DOI":"10.1155\/2012\/509465"},{"key":"18_CR49","doi-asserted-by":"publisher","unstructured":"IEEE Standard for VHDL Language Reference Manual (2019). https:\/\/doi.org\/10.1109\/IEEESTD.2019.8938196","DOI":"10.1109\/IEEESTD.2019.8938196"},{"key":"18_CR50","doi-asserted-by":"publisher","unstructured":"Waddoups, N., et al.: Artifact for \u201cprobabilistic verification for modular network-on-chip systems artifact\u201d submitted to vmcai26 (2025). https:\/\/doi.org\/10.5281\/zenodo.17247418","DOI":"10.5281\/zenodo.17247418"},{"key":"18_CR51","unstructured":"Waddoups, N., et al.: Probabilistic verification for modular network-on-chip systems (extended version) (2025). https:\/\/arxiv.org\/abs\/2511.13890"},{"key":"18_CR52","doi-asserted-by":"publisher","unstructured":"Wang, L., Cai, F.: Reliability analysis for flight control systems using probabilistic model checking. In: 2017 8th IEEE International Conference on Software Engineering and Service Science (ICSESS), pp. 161\u2013164 (2017). https:\/\/doi.org\/10.1109\/ICSESS.2017.8342887","DOI":"10.1109\/ICSESS.2017.8342887"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15700-3_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:21:49Z","timestamp":1768202509000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15700-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032156990","9783032157003"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15700-3_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"13 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rennes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}