{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:00:29Z","timestamp":1743026429757,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031826993"},{"type":"electronic","value":"9783031827006"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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-82700-6_3","type":"book-chapter","created":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T01:26:36Z","timestamp":1737595596000},"page":"52-73","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Property-Agnostic Base Case Extension for Scalable Verification of Distributed Systems"],"prefix":"10.1007","author":[{"given":"Kyle","family":"Storey","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2264-2958","authenticated-orcid":false,"given":"Eric","family":"Mercer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,1,24]]},"reference":[{"issue":"5","key":"3_CR1","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s10009-015-0406-x","volume":"18","author":"P Abdulla","year":"2016","unstructured":"Abdulla, P., Haziza, F., Hol\u00edk, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transf. 18(5), 495\u2013516 (2016). https:\/\/doi.org\/10.1007\/s10009-015-0406-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR2","unstructured":"Athalye, A.: CoqIOA : a formalization of IO automata in the Coq proof assistant. Master\u2019s thesis, Massachusetts Institute of Technology (2017)"},{"key":"3_CR3","unstructured":"Bateman, K.: MyCHIPs digital money (2023). http:\/\/gotchoices.org\/mychips\/intro.html"},{"key":"3_CR4","unstructured":"Bateman, K.: MyCHIPs protocol description 1.3. MyCHIPs Protocol Description 1.3 (2023). https:\/\/github.com\/gotchoices\/MyCHIPs\/blob\/master\/doc\/learn-protocol.md"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Bozga, M., Iosif, R., Sifakis, J.: Verification of component-based systems with recursive architectures. Theoret. Comput. Sci. 940, 146\u2013175 (2023). https:\/\/doi.org\/10.1016\/j.tcs.2022.10.022. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397522006181","DOI":"10.1016\/j.tcs.2022.10.022"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing, PODC 1986, pp. 240\u2013248. Association for Computing Machinery, New York (1986). https:\/\/doi.org\/10.1145\/10590.10611","DOI":"10.1145\/10590.10611"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"131","DOI":"10.4204\/eptcs.161.13","volume":"161","author":"G Delzanno","year":"2014","unstructured":"Delzanno, G., Tatarek, M., Traverso, R.: Model checking Paxos in Spin. Electron. Proc. Theor. Comput. Sci. 161, 131\u2013146 (2014). https:\/\/doi.org\/10.4204\/eptcs.161.13","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"3_CR8","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/6874.001.0001","volume-title":"Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits","author":"DL Dill","year":"1989","unstructured":"Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits, vol. 24. MIT Press, Cambridge (1989)"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Driscoll, E., Burton, A., Reps, T.: Checking conformance of a producer and a consumer. In: Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, ESEC\/FSE 2011, pp. 113\u2013123. Association for Computing Machinery, New York (2011). https:\/\/doi.org\/10.1145\/2025113.2025132","DOI":"10.1145\/2025113.2025132"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. In: Proceedings of the 2nd ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, PODS 1983, pp. 1\u20137. Association for Computing Machinery, New York (1983). https:\/\/doi.org\/10.1145\/588058.588060","DOI":"10.1145\/588058.588060"},{"issue":"3","key":"3_CR11","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992). https:\/\/doi.org\/10.1145\/146637.146681","journal-title":"J. ACM"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/3-540-08755-9_9","volume-title":"Operating Systems","author":"JN Gray","year":"1978","unstructured":"Gray, J.N.: Notes on data base operating systems. In: Bayer, R., Graham, R.M., Seegm\u00fcller, G. (eds.) Operating Systems. LNCS, vol. 60, pp. 393\u2013481. Springer, Heidelberg (1978). https:\/\/doi.org\/10.1007\/3-540-08755-9_9"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Huang, Y., Ogles, B., Mercer, E.: A predictive analysis for detecting deadlock in MPI programs. In: 2020 35th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 18\u201328 (2020)","DOI":"10.1145\/3324884.3416588"},{"issue":"2","key":"3_CR14","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/s10009-022-00648-0","volume":"24","author":"G Lowe","year":"2022","unstructured":"Lowe, G.: Parameterized verification of systems with component identities using view abstraction. Int. J. Softw. Tools Technol. Transf. 24(2), 287\u2013324 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00648-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Ogles, B., Aldous, P., Mercer, E.: Proving data race freedom in task parallel programs using a weaker partial order. In: 2019 Formal Methods in Computer Aided Design (FMCAD), pp. 55\u201363 (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894270","DOI":"10.23919\/FMCAD.2019.8894270"},{"key":"3_CR16","unstructured":"Ozanne, L.: Learning to exchange time: Benefits and obstacles to time banking. Int. J. Community Currency Res. 14 (2010)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-45657-0_13","volume-title":"Computer Aided Verification","author":"SK Rajamani","year":"2002","unstructured":"Rajamani, S.K., Rehof, J.: Conformance checking for models of asynchronous message passing software. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 166\u2013179. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_13"},{"issue":"4","key":"3_CR18","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1145\/98163.98167","volume":"22","author":"FB Schneider","year":"1990","unstructured":"Schneider, F.B.: Implementing fault-tolerant services using the state machine approach: a tutorial. ACM Comput. Surv. 22(4), 299\u2013319 (1990). https:\/\/doi.org\/10.1145\/98163.98167","journal-title":"ACM Comput. Surv."},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Schuppan, V., Biere, A.: Liveness checking as safety checking for infinite state spaces. Electron. Notes Theor. Comput. Sci. 149(1), 79\u201396 (2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.11.018. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066106000557. Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY 2005)","DOI":"10.1016\/j.entcs.2005.11.018"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Valek, L.: The time bank implementation and governance: Is PRINCE 2 suitable? Procedia Technol. 16, 950\u2013956 (2014). https:\/\/doi.org\/10.1016\/j.protcy.2014.10.048. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S2212017314002758","DOI":"10.1016\/j.protcy.2014.10.048"}],"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-031-82700-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T01:26:42Z","timestamp":1737595602000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-82700-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031826993","9783031827006"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-82700-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"24 January 2025","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":"Denver, CO","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 January 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 January 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}