{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T16:08:12Z","timestamp":1779034092549,"version":"3.51.4"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Today\u2019s distributed systems operate in complex environments that inevitably involve faults and even adversarial behaviors. Predicting their performance under such environments directly from formal designs remains a long-standing challenge. We present the first formal framework that systematically enables performance prediction of distributed systems across diverse faulty scenarios. Our framework features a fault injector together with a wide range of faults, reusable as a library,\u00a0and model compositions that integrate the system and the fault injector into a unified model suitable for statistical analysis of performance properties such as throughput and latency. We formalize the framework in Maude and implement it as an automated tool,\n                    <jats:sc>PerF<\/jats:sc>\n                    . Applied to representative distributed systems,\n                    <jats:sc>PerF<\/jats:sc>\n                    accurately predicts system performance under varying fault settings, with estimations from formal designs consistent with evaluations on real deployments.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_3","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:34Z","timestamp":1779033034000},"page":"47-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Formal Framework for\u00a0Predicting Distributed System Performance Under Faults"],"prefix":"10.1007","author":[{"given":"Ziwei","family":"Zhou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Si","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhou","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peixin","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Min","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"3_CR1","unstructured":"Apache Cassandra: Open Source NoSQL Database (Nov 2025). https:\/\/cassandra.apache.org\/"},{"key":"3_CR2","unstructured":"AWS Fault Injection Service (Nov 2025). https:\/\/aws.amazon.com\/fis\/"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, USA (1986)","DOI":"10.7551\/mitpress\/1086.001.0001"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci. 153(2) (2006)","DOI":"10.1016\/j.entcs.2005.10.040"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1) (2018)","DOI":"10.1145\/3158668"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-22944-2_28","volume-title":"Algebra and Coalgebra in Computer Science","author":"M AlTurki","year":"2011","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386\u2013392. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22944-2_28"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"AlTurki, M.A., Kanovich, M.I., Kirigin, T.B., Nigam, V., Scedrov, A., Talcott, C.L.: Statistical model checking of distance fraud attacks on the Hancke-Kuhn family of protocols. In: CPS-SPC@CCS 2018, pp. 60\u201371. ACM (2018)","DOI":"10.1145\/3264888.3264895"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-030-54994-7_25","volume-title":"Formal Methods. FM 2019 International Workshops","author":"MA Alturki","year":"2020","unstructured":"Alturki, M.A., Ro\u015fu, G.: Statistical model checking of RANDAO\u2019s resilience to pre-computed reveal strategies. In: Sekerinski, E., et al. (eds.) FM 2019. LNCS, vol. 12232, pp. 337\u2013349. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-54994-7_25"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Theory in practice for system design and verification. ACM SIGLOG News 2(1) (2015)","DOI":"10.1145\/2728816.2728827"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Bailis, P., Fekete, A., Ghodsi, A., Hellerstein, J.M., Stoica, I.: Scalable atomic visibility with RAMP transactions. ACM Trans. Database Syst. 41(3), 15:1\u201315:45 (2016)","DOI":"10.1145\/2909870"},{"key":"3_CR11","unstructured":"Bano, S., Sonnino, A., Chursin, A., Perelman, D., Li, Z., Ching, A., Malkhi, D.: Twins: BFT systems made robust. In: OPODIS 2021. Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0217, pp. 7:1\u20137:29 (2022)"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Benson, T., Akella, A., Maltz, D.A.: Network traffic characteristics of data centers in the wild. In: IMC 2010, pp. 267\u2013280. ACM (2010)","DOI":"10.1145\/1879141.1879175"},{"key":"3_CR13","unstructured":"Bernstein, P.A., Hadzilacos, V., Goodman, N.: Concurrency Control and Recovery in Database Systems. Addison-Wesley (1987)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Bobba, R., Grov, J., Gupta, I., Liu, S., Meseguer, J., \u00d6lveczky, P.C., Skeirik, S.: Survivability: design, formal modeling, and validation of cloud storage systems using Maude. Assured Cloud Comput., 10\u201348 (2018)","DOI":"10.1002\/9781119428497.ch2"},{"key":"3_CR15","unstructured":"Brooker, M.: Fifteen years of formal methods at AWS. TLA+ Conference (2024). https:\/\/conf.tlapl.us\/2024\/MarcBrooker-FifteenYearsOfTLAPlus.pdf"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay, A., Wang, Z.: UPPAAL-SMC: statistical model checking for priced timed automata. In: QAPL 2012. EPTCS, vol.\u00a085, pp. 1\u201316 (2012)","DOI":"10.4204\/EPTCS.85.1"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Chen, H., Dou, W., Wang, D., Qin, F.: CoFI: consistency-guided fault injection for cloud systems. In: ASE 2020, pp. 536\u2013547 (2020)","DOI":"10.1145\/3324884.3416548"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Chen, Y., Ma, F., Zhou, Y., Gu, M., Liao, Q., Jiang, Y.: Chronos: finding timeout bugs in practical distributed systems by deep-priority fuzzing with transient delay. In: IEEE Symposium on Security and Privacy (SP), IEEE Computer Society (2024)","DOI":"10.1109\/SP54263.2024.00109"},{"issue":"12","key":"3_CR19","doi-asserted-by":"publisher","first-page":"3014","DOI":"10.14778\/3476311.3476379","volume":"14","author":"A Cheng","year":"2021","unstructured":"Cheng, A., et al.: RAMP-TAO: layering atomic transactions on facebook\u2019s online TAO data store. Proc. VLDB Endow. 14(12), 3014\u20133027 (2021)","journal-title":"Proc. VLDB Endow."},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Chuat, L., Legner, M., Basin, D.A., Hausheer, D., Hitz, S., M\u00fcller, P., Perrig, A.: The Complete Guide to SCION - From Design Principles to Formal Verification. Springer, Information Security and Cryptography (2022). https:\/\/doi.org\/10.1007\/978-3-031-05288-0","DOI":"10.1007\/978-3-031-05288-0"},{"key":"3_CR21","unstructured":"Clavel, M., et al.: All About Maude, LNCS, vol.\u00a04350. Springer (2007)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Cooper, B.F., Silberstein, A., Tam, E., Ramakrishnan, R., Sears, R.: Benchmarking cloud serving systems with YCSB. In: SoCC 2010, pp. 143\u2013154. ACM (2010)","DOI":"10.1145\/1807128.1807152"},{"issue":"1","key":"3_CR23","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1109\/18.61110","volume":"37","author":"RL Cruz","year":"1991","unstructured":"Cruz, R.L.: A calculus for network delay, part II: network analysis. IEEE Trans. Inf. Theory 37(1), 132\u2013141 (1991)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"3_CR24","unstructured":"Davis, A.J.J.: Are we serious about using TLA+ for statistical properties? TLA+ Community Event (2025). https:\/\/conf.tlapl.us\/2025-etaps\/davis-slides.pdf"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-642-28872-2_6","volume-title":"Fundamental Approaches to Software Engineering","author":"J Eckhardt","year":"2012","unstructured":"Eckhardt, J., M\u00fchlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M.: Stable availability under denial of service attacks through formal patterns. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 78\u201393. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_6"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Gao, Y., Dou, W., Wang, D., Feng, W., Wei, J., Zhong, H., Huang, T.: Coverage guided fault injection for cloud systems. In: 2023 IEEE\/ACM 45th International Conference on Software Engineering (ICSE), pp. 2211\u20132223 (2023)","DOI":"10.1109\/ICSE48619.2023.00186"},{"issue":"2","key":"3_CR27","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"JA Goguen","year":"1992","unstructured":"Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105(2), 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","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"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Jaffe, A., Moscibroda, T., Sen, S.: On the price of equivocation in byzantine agreement. In: PODC 2012, pp. 309\u2013318. ACM (2012)","DOI":"10.1145\/2332432.2332491"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Jalalzai, M.M., Niu, J., Feng, C., Gai, F.: Fast-HotStuff: a fast and robust BFT protocol for blockchains. IEEE Trans. Dependable Sec. Comput., 1\u201317 (2023)","DOI":"10.1109\/TDSC.2023.3308848"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Jang, K., Sherry, J., Ballani, H., Moncaster, T.: Silo: predictable message latency in the cloud. In: SIGCOMM 2015, pp. 435\u2013448. ACM (2015)","DOI":"10.1145\/2785956.2787479"},{"key":"3_CR32","unstructured":"Jepsen: A framework for distributed systems verification, with fault injection (Nov 2025). http:\/\/jepsen.io\/"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","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"},{"key":"3_CR34","unstructured":"Lamport, L.: Specifying Systems. The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Liang, L., Liu, S.: Exploring design alternatives for replicated RAMP transactions using Maude. In: TASE 2021, pp. 111\u2013118. IEEE (2021)","DOI":"10.1109\/TASE52547.2021.00026"},{"issue":"2","key":"3_CR36","doi-asserted-by":"publisher","first-page":"1010","DOI":"10.1109\/TIT.2011.2173713","volume":"58","author":"J Liebeherr","year":"2012","unstructured":"Liebeherr, J., Burchard, A., Ciucu, F.: Delay bounds in communication networks with heavy-tailed and self-similar traffic. IEEE Trans. Inf. Theory 58(2), 1010\u20131024 (2012)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Liu, S.: All in one: Design, verification, and implementation of SNOW-optimal read atomic transactions. ACM Trans. Softw. Eng. Methodol. 31(3) (2022)","DOI":"10.1145\/3494517"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Liu, S., Duan, H., Heimes, L., Bearzi, M., Vieli, J., Basin, D., Perrig, A.: A formal framework for end-to-end DNS resolution. In: SIGCOMM 2023, pp. 932\u2013949. ACM (2023)","DOI":"10.1145\/3603269.3604870"},{"key":"3_CR39","unstructured":"Liu, S., Ganhotra, J., Rahman, M.R., Nguyen, S., Gupta, I., Meseguer, J.: Quantitative analysis of consistency in NoSQL key-value stores. Leibniz Trans. Embed. Syst. 4(1), 03:1\u201303:26 (2017)"},{"issue":"OOPSLA2","key":"3_CR40","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1145\/3563299","volume":"6","author":"S Liu","year":"2022","unstructured":"Liu, S., Meseguer, J., \u00d6lveczky, P.C., Zhang, M., Basin, D.A.: Bridging the semantic gap between qualitative and quantitative models of distributed systems. Proc. ACM Program. Lang. 6(OOPSLA2), 315\u2013344 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-319-68690-5_18","volume-title":"Formal Methods and Software Engineering","author":"S Liu","year":"2017","unstructured":"Liu, S., \u00d6lveczky, P.C., Ganhotra, J., Gupta, I., Meseguer, J.: Exploring design alternatives for ramp transactions through statistical model\u00a0checking. In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 298\u2013314. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68690-5_18"},{"issue":"5","key":"3_CR42","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/s00165-019-00489-w","volume":"31","author":"S Liu","year":"2019","unstructured":"Liu, S., \u00d6lveczky, P.C., Wang, Q., Gupta, I., Meseguer, J.: Read atomic transactions with prevention of lost updates: ROLA and its formal analysis. Formal Aspects Comput. 31(5), 503\u2013540 (2019)","journal-title":"Formal Aspects Comput."},{"key":"3_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-319-99840-4_8","volume-title":"Rewriting Logic and Its Applications","author":"S Liu","year":"2018","unstructured":"Liu, S., \u00d6lveczky, P.C., Wang, Q., Meseguer, J.: Formal modeling and analysis of the walter transactional data store. In: Rusu, V. (ed.) WRLA 2018. LNCS, vol. 11152, pp. 136\u2013152. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99840-4_8"},{"key":"3_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-030-55754-6_2","volume-title":"NASA Formal Methods","author":"S Liu","year":"2020","unstructured":"Liu, S., Sandur, A., Meseguer, J., \u00d6lveczky, P.C., Wang, Q.: Generating correct-by-construction distributed implementations from formal maude designs. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 22\u201340. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_2"},{"key":"3_CR45","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann (1996)"},{"key":"3_CR46","unstructured":"Maude: Applications (Nov 2025). https:\/\/maude.cs.illinois.edu\/wiki\/Applications"},{"issue":"1","key":"3_CR47","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR48","doi-asserted-by":"publisher","unstructured":"Meseguer, J.: Capturing system designs with formal executable specifications. In: FASE 2025, LNCS, vol. 15693, pp. 1\u201332. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90900-9_1","DOI":"10.1007\/978-3-031-90900-9_1"},{"key":"3_CR49","unstructured":"Netflix: Chaos Monkey (Nov 2025). https:\/\/netflix.github.io\/chaosmonkey\/"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon Web Services uses formal methods. Commun. ACM (2015)","DOI":"10.1145\/2699417"},{"key":"3_CR51","unstructured":"Ongaro, D., Ousterhout, J.: In search of an understandable consensus algorithm. In: USENIX ATC 2014, pp. 305\u2013320. USENIX Association (2014)"},{"key":"3_CR52","unstructured":"PowerDNS: PowerDNS: a faster, safer, and more secure internet (Nov 2025). https:\/\/www.powerdns.com\/"},{"key":"3_CR53","doi-asserted-by":"publisher","unstructured":"Rubio, R., Mart\u00ed-Oliet, N., Pita, I., Verdejo, A.: QMaude: quantitative specification and verification in rewriting logic. In: FM 2023. LNCS, vol. 14000, pp. 240\u2013259. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_15","DOI":"10.1007\/978-3-031-27481-7_15"},{"key":"3_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266\u2013280. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_26"},{"key":"3_CR55","unstructured":"Tanenbaum, A.S., van Steen, M.: Distributed systems - principles and paradigms, 2nd Edition. Pearson Education (2007)"},{"key":"3_CR56","unstructured":"Vanlightly, J., Kuppe, M.: Obtaining statistical properties via TLC simulation. TLA+ Conference (2022). https:\/\/conf.tlapl.us\/2022\/JackMarkusTLA+Statistics.pdf"},{"key":"3_CR57","doi-asserted-by":"crossref","unstructured":"Weghorn, T., Liu, S., Sprenger, C., Perrig, A., Basin, D.A.: N-Tube: formally verified secure bandwidth reservation in path-aware Internet architectures. In: CSF 2022, pp. 147\u2013162. IEEE (2022)","DOI":"10.1109\/CSF54842.2022.9919646"},{"key":"3_CR58","doi-asserted-by":"crossref","unstructured":"White, B., et al.: An integrated experimental environment for distributed systems and networks. In: OSDI 2002. USENIX Association (2002)","DOI":"10.1145\/1060289.1060313"},{"issue":"OOPSLA1","key":"3_CR59","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1145\/3586053","volume":"7","author":"LN Winter","year":"2023","unstructured":"Winter, L.N., Buse, F., de Graaf, D., von Gleissenthall, K., Ozkan, B.K.: Randomized testing of Byzantine fault tolerant algorithms. Proc. ACM Program. Lang. 7(OOPSLA1), 757\u2013788 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"3_CR60","doi-asserted-by":"crossref","unstructured":"Zhang, T.N., Sharma, U., Kapritsos, M.: Performal: formal verification of latency properties for distributed systems. Proc. ACM Program. Lang. 7(PLDI) (2023)","DOI":"10.1145\/3591235"},{"key":"3_CR61","unstructured":"Zhou, Z., Liu, S., Zhou, Z., Wang, P., Zhang, M.: A Formal Framework for Predicting Distributed System Performance under Faults (Extended Version). Tech. rep. (2026). https:\/\/arxiv.org\/abs\/2602.19088"},{"key":"3_CR62","unstructured":"Zhou, Z., Liu, S., Zhou, Z., Wang, P., Zhang, M.: Artifact for \u201cA Formal Framework for Predicting Distributed System Performance under Faults (2026). https:\/\/doi.org\/10.5281\/zenodo.18619604"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:50:39Z","timestamp":1779033039000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_3","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":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","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":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 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":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}