{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,8]],"date-time":"2025-11-08T17:41:59Z","timestamp":1762623719232,"version":"3.41.0"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319254227"},{"type":"electronic","value":"9783319254234"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25423-4_14","type":"book-chapter","created":{"date-parts":[[2015,11,30]],"date-time":"2015-11-30T17:10:46Z","timestamp":1448903446000},"page":"217-233","source":"Crossref","is-referenced-by-count":16,"title":["History-Based Specification and Verification of Scalable Concurrent and Distributed Systems"],"prefix":"10.1007","author":[{"given":"Crystal Chang","family":"Din","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S. Lizeth","family":"Tapia Tarifa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,1]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1086.001.0001","volume-title":"ACTORS: A Model of Concurrent Computations in Distributed Systems","author":"GA Agha","year":"1986","unstructured":"Agha, G.A.: ACTORS: A Model of Concurrent Computations in Distributed Systems. The MIT Press, Cambridge (1986)"},{"issue":"12","key":"14_CR2","doi-asserted-by":"publisher","first-page":"1289","DOI":"10.1016\/j.scico.2010.08.003","volume":"77","author":"W Ahrendt","year":"2012","unstructured":"Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Sci. Comput. Program. 77(12), 1289\u20131309 (2012)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"14_CR3","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s11761-013-0148-0","volume":"8","author":"E Albert","year":"2014","unstructured":"Albert, E., de Boer, F.S., H\u00e4hnle, R., Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L., Wong, P.Y.H.: Formal modeling of resource management for cloud architectures: an industrial case study using real-time ABS. J. SOCA 8(4), 323\u2013339 (2014)","journal-title":"J. SOCA"},{"issue":"4","key":"14_CR4","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"14_CR5","first-page":"1","volume":"11","author":"A Amighi","year":"2015","unstructured":"Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11, 1\u201366 (2015)","journal-title":"LMCS"},{"issue":"3","key":"14_CR6","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"KR Apt","year":"1980","unstructured":"Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM TOPLAS 2(3), 359\u2013385 (1980)","journal-title":"ACM TOPLAS"},{"key":"14_CR7","unstructured":"Armstrong, J.: Programming Erlang. Pragmatic Bookshelf (2007)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)"},{"issue":"1","key":"14_CR9","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/s11334-012-0184-5","volume":"9","author":"J Bj\u00f8rk","year":"2013","unstructured":"Bj\u00f8rk, J., de Boer, F.S., Johnsen, E.B., Schlatte, R., Tapia, S.L.: User-defined schedulers for real-time concurrent objects. Innovations Syst. Softw. Eng. 9(1), 29\u201343 (2013)","journal-title":"Innovations Syst. Softw. Eng."},{"key":"14_CR10","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1155\/2009\/548324","volume":"2009","author":"D Borrione","year":"2009","unstructured":"Borrione, D., Helmy, A., Pierre, L., Schmaltz, J.: A formal approach to the verification of networks on chip. EURASIP J. Embed. Syst. 2009, 2:1\u20132:14 (2009)","journal-title":"EURASIP J. Embed. Syst."},{"issue":"2","key":"14_CR11","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/s10703-011-0134-0","volume":"40","author":"S Chatterjee","year":"2012","unstructured":"Chatterjee, S., Kishinevsky, M.: Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics. Formal Methods Syst. Des. 40(2), 147\u2013169 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR12","unstructured":"Dahl, O.-J.: Can program proving be made practical? In: Les Fondements de la Programmation, pp. 57\u2013114. IRIA, December 1977"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-540-71316-6_22","volume-title":"Programming Languages and Systems","author":"FS Boer de","year":"2007","unstructured":"de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316\u2013330. Springer, Heidelberg (2007)"},{"issue":"3","key":"14_CR14","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1109\/MDT.2012.2205998","volume":"29","author":"S Chatterjee","year":"2012","unstructured":"Chatterjee, S., Kishinevsky, M., Ogras, \u00dc.Y.: xMAS: quick formal modeling of communication fabrics to enable verification. IEEE Des. Test Comput. 29(3), 80\u201388 (2012)","journal-title":"IEEE Des. Test Comput."},{"issue":"3","key":"14_CR15","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.jlap.2012.01.003","volume":"81","author":"CC Din","year":"2012","unstructured":"Din, C.C., Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of distributed systems: component reasoning for concurrent objects. J. Logic Algebraic Program. 81(3), 227\u2013256 (2012)","journal-title":"J. Logic Algebraic Program."},{"issue":"5\u20136","key":"14_CR16","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1016\/j.jlamp.2014.03.003","volume":"83","author":"CC Din","year":"2014","unstructured":"Din, C.C., Owe, O.: A sound and complete reasoning system for asynchronous communication with shared futures. J. Logical Algebraic Methods Program. 83(5\u20136), 360\u2013383 (2014)","journal-title":"J. Logical Algebraic Methods Program."},{"issue":"3","key":"14_CR17","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/s00165-014-0322-y","volume":"27","author":"CC Din","year":"2015","unstructured":"Din, C.C., Owe, O.: Compositional reasoning about active objects with shared futures. Formal Aspects Comput. 27(3), 551\u2013572 (2015)","journal-title":"Formal Aspects Comput."},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-319-21401-6_35","volume-title":"Automated Deduction - CADE-25","author":"CC Din","year":"2015","unstructured":"Din, C.C., Bubel, R., H\u00e4hnle, R.: KeY-ABS: a deductive verification tool for the concurrent modelling language ABS. In: Felty, A., Middeldorp, A. (eds.) Automated Deduction - CADE-25. LNCS, vol. 9195, pp. 517\u2013526. Springer, Switzerland (2015)"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Dovland, J., Johnsen, E.B., Owe, O.: Verification of concurrent objects with asynchronous method calls. In: Proceedings of International Conference on Software Science, Technology & Engineering (SwSTE 2005), pp. 141\u2013150. IEEE Press, February 2005","DOI":"10.1109\/SWSTE.2005.24"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Giachino, E., Laneve, C., Lienhardt, M.: A framework for deadlock detection in core ABS. Softw. Syst. Model. 1\u201336 (2015). Springer. doi: 10.1007\/s10270-014-0444-y","DOI":"10.1007\/s10270-014-0444-y"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-35873-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Heule","year":"2013","unstructured":"Heule, S., Leino, K.R.M., M\u00fcller, P., Summers, A.J.: Abstract read permissions: fractional permissions without the fractions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 315\u2013334. Springer, Heidelberg (2013)"},{"key":"14_CR22","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Upper Saddle River (1985)"},{"issue":"9","key":"14_CR23","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TCAD.2014.2331342","volume":"33","author":"DE Holcomb","year":"2014","unstructured":"Holcomb, D.E., Seshia, S.A.: Compositional performance verification of network-on-chip designs. IEEE Trans. CAD Integr. Circ. Syst. 33(9), 1370\u20131383 (2014)","journal-title":"IEEE Trans. CAD Integr. Circ. Syst."},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Piessens, F., Leino, K.R.M., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: Proceedings of SEFM, pp. 137\u2013147. IEEE (2005)","DOI":"10.1109\/SEFM.2005.39"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-540-31987-0_29","volume-title":"Programming Languages and Systems","author":"A Jeffrey","year":"2005","unstructured":"Jeffrey, A., Rathke, J.: Java JR: fully abstract trace semantics for a core Java language. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 423\u2013438. Springer, Heidelberg (2005)"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011)"},{"issue":"1","key":"14_CR27","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10270-006-0011-2","volume":"6","author":"EB Johnsen","year":"2007","unstructured":"Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Softw. Syst. Model. 6(1), 35\u201358 (2007)","journal-title":"Softw. Syst. Model."},{"key":"14_CR28","unstructured":"Jones, C.B.: Development methods for computer programmes including a notion of interference. Ph.D. thesis, Oxford University, UK, June l981"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-29320-7_16","volume-title":"Fundamentals of Software Engineering","author":"M Kamali","year":"2012","unstructured":"Kamali, M., Petre, L., Sere, K., Daneshtalab, M.: Refinement-based modeling of 3D NoCs. In: Arbab, F., Sirjani, M. (eds.) FSEN 2011. LNCS, vol. 7141, pp. 236\u2013252. Springer, Heidelberg (2012)"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Kumar, S., Jantsch, A., Millberg, M., \u00d6berg, J., Soininen, J., Forsell, M., Tiensyrj\u00e4, K., Hemani, A.: A network on chip architecture and design methodology. In: Proceedings of VLSI, pp. 117\u2013124 (2002)","DOI":"10.1109\/ISVLSI.2002.1016885"},{"key":"14_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-03829-7_7","volume-title":"Foundations of Security Analysis and Design V","author":"KRM Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) Foundations of Security Analysis and Design V. LNCS, vol. 5705, p. 195. Springer, Heidelberg (2009)"},{"key":"14_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","volume":"4","author":"R Milner","year":"1977","unstructured":"Milner, R.: Fully abstract models of typed $$\\lambda $$ \u03bb -calculi. Theoret. Comput. Sci. 4, 1\u201322 (1977)","journal-title":"Theoret. Comput. Sci."},{"issue":"4","key":"14_CR33","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng. 7(4), 417\u2013426 (1981)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"14_CR34","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"key":"14_CR35","unstructured":"Sharifi, Z., Mohammadi, S., Sirjani, M.: Comparison of NoC routing algorithms using formal methods. In: Proceedings of Parallel and Distributed Processing Techniques and Applications (PDPTA 2013), vol. 2, pp. 474\u2013482. CSREA Press (2013)"},{"key":"14_CR36","unstructured":"Sharifi, Z., Mosaffa, M., Mohammadi, S., Sirjani, M.: Functional and performance analysis of network-on-chips using actor-based modeling and formal verification. ECEASST 66, 16 (2013)"},{"issue":"6","key":"14_CR37","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1109\/MDT.2008.167","volume":"25","author":"A Sheibanyrad","year":"2008","unstructured":"Sheibanyrad, A., Greiner, A., Panades, I.M.: Multisynchronous and fully asynchronous NoCs for GALS architectures. IEEE Des. Test Comput. 25(6), 572\u2013580 (2008)","journal-title":"IEEE Des. Test Comput."},{"key":"14_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-24933-4_3","volume-title":"Formal Modeling: Actors, Open Systems, Biological Systems","author":"M Sirjani","year":"2011","unstructured":"Sirjani, M., Jaghoori, M.M.: Ten years of analyzing actors: Rebeca experience. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 20\u201356. Springer, Heidelberg (2011)"},{"issue":"4","key":"14_CR39","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1145\/1780.1805","volume":"6","author":"N Soundararajan","year":"1984","unstructured":"Soundararajan, N.: Axiomatic semantics of communicating sequential processes. ACM TOPLAS 6(4), 647\u2013662 (1984)","journal-title":"ACM TOPLAS"},{"key":"14_CR40","unstructured":"Verbeek, F., Schmaltz, J.: Hunting deadlocks efficiently in microarchitectural models of communication fabrics. In: International Conference on Formal Methods in Computer-Aided Design (FMCAD 2011), pp. 223\u2013231. FMCAD Inc. (2011)"},{"issue":"5","key":"14_CR41","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/s10009-012-0250-1","volume":"14","author":"PYH Wong","year":"2012","unstructured":"Wong, P.Y.H., Albert, E., Muschevici, R., Proen\u00e7a, J., Sch\u00e4fer, J., Schlatte, R.: The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. STTT 14(5), 567\u2013588 (2012)","journal-title":"STTT"},{"key":"14_CR42","doi-asserted-by":"crossref","unstructured":"Zaharieva-Stojanovski, M., Huisman, M., Blom, S.: Verifying functional behaviour of concurrent programs. In: Proceedings of 16th Workshop on Formal Techniques for Java-Like Programs (FTfJP 2014), pp. 4:1\u20134:6. ACM (2014)","DOI":"10.1145\/2635631.2635849"},{"key":"14_CR43","series-title":"Lecture Notes in Computer Science","volume-title":"Compositionality, Concurrency and Partial Correctness: Proof Theories for Networks of Processes, and Their Relationship","author":"J Zwiers","year":"1989","unstructured":"Zwiers, J.: Compositionality, Concurrency and Partial Correctness: Proof Theories for Networks of Processes, and Their Relationship. LNCS, vol. 321. Springer, Heidelberg (1989)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25423-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T16:15:36Z","timestamp":1748708136000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25423-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319254227","9783319254234"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25423-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}