{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:49:45Z","timestamp":1742917785382,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031081651"},{"type":"electronic","value":"9783031081668"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-08166-8_1","type":"book-chapter","created":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:03:27Z","timestamp":1656889407000},"page":"1-18","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["I Can See Clearly Now: Clairvoyant Assertions for\u00a0Deadlock Checking"],"prefix":"10.1007","author":[{"given":"Ole J\u00f8rgen","family":"Abusdal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Crystal Chang","family":"Din","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Violet Ka I","family":"Pun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Volker","family":"Stolz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,7,4]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification - The KeY Book - From Theory to Practice","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64354-6","volume-title":"Deductive Software Verification: Future Perspectives","year":"2020","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Ulbrich, M. (eds.): Deductive Software Verification: Future Perspectives. LNCS, vol. 12345. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Albert, E., Flores-Montoya, A., Genaim, S., Martin-Martin, E.: May-happen-in-parallel analysis for actor-based concurrency. ACM Trans. Comput. Log. 17(2), 11:1\u201311:39 (2016). https:\/\/doi.org\/10.1145\/2824255","DOI":"10.1145\/2824255"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-07317-0_1","volume-title":"Formal Methods for Executable Software Models","author":"R Bubel","year":"2014","unstructured":"Bubel, R., Montoya, A.F., H\u00e4hnle, R.: Analysis of executable software models. In: Bernardo, M., Damiani, F., H\u00e4hnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 1\u201325. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07317-0_1"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342\u2013363. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_16"},{"issue":"6","key":"1_CR6","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1002\/spe.649","volume":"35","author":"Y Cheon","year":"2005","unstructured":"Cheon, Y., Leavens, G.T., Sitaraman, M., Edwards, S.H.: Model variables: cleanly supporting abstraction in design by contract. Softw. Pract. Exp. 35(6), 583\u2013599 (2005). https:\/\/doi.org\/10.1002\/spe.649","journal-title":"Softw. Pract. Exp."},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 517\u2013526. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_35"},{"issue":"3","key":"1_CR8","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/s00165-014-0322-y","volume":"27","author":"CC Din","year":"2014","unstructured":"Din, C.C., Owe, O.: Compositional reasoning about active objects with shared futures. Formal Aspects Comput. 27(3), 551\u2013572 (2014). https:\/\/doi.org\/10.1007\/s00165-014-0322-y","journal-title":"Formal Aspects Comput."},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-319-47166-2_36","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"AM Eilertsen","year":"2016","unstructured":"Eilertsen, A.M., Bagge, A.H., Stolz, V.: Safer refactorings. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 517\u2013531. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_36"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Knoop, J., Hendren, L.J. (eds.) Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 234\u2013245. ACM (2002). https:\/\/doi.org\/10.1145\/512529.512558","DOI":"10.1145\/512529.512558"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/11554554_10","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"T Gedell","year":"2005","unstructured":"Gedell, T.: Embedding static analysis into tableaux and sequent based frameworks. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 108\u2013122. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11554554_10"},{"issue":"4","key":"1_CR12","doi-asserted-by":"publisher","first-page":"1013","DOI":"10.1007\/s10270-014-0444-y","volume":"15","author":"E Giachino","year":"2016","unstructured":"Giachino, E., Laneve, C., Lienhardt, M.: A framework for deadlock detection in core ABS. Softw. Syst. Model. 15(4), 1013\u20131048 (2016). https:\/\/doi.org\/10.1007\/s10270-014-0444-y","journal-title":"Softw. Syst. Model."},{"key":"1_CR13","doi-asserted-by":"publisher","first-page":"46033","DOI":"10.1109\/ACCESS.2021.3065421","volume":"9","author":"M G\u00f3mez-Zamalloa","year":"2021","unstructured":"G\u00f3mez-Zamalloa, M., Isabel, M.: Deadlock-guided testing. IEEE Access 9, 46033\u201346048 (2021). https:\/\/doi.org\/10.1109\/ACCESS.2021.3065421","journal-title":"IEEE Access"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-40615-7_1","volume-title":"Formal Methods for Components and Objects","author":"R H\u00e4hnle","year":"2013","unstructured":"H\u00e4hnle, R.: The abstract behavioral specification language: a tutorial introduction. In: Giachino, E., H\u00e4hnle, R., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2012. LNCS, vol. 7866, pp. 1\u201337. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40615-7_1"},{"key":"1_CR15","unstructured":"Hewitt, C., Bishop, P., Steiger, R.: A universal modular ACTOR formalism for artificial intelligence. In: Proceedings of the International Joint Conference on Artificial Intelligence, pp. 235\u2013245. Morgan Kaufmann Publishers Inc. (1973). http:\/\/dl.acm.org\/citation.cfm?id=1624775.1624804"},{"key":"1_CR16","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.) FMCO 2010. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25271-6_8"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Kamburjan, E.: Detecting deadlocks in formal system models with condition synchronization. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 76 (2018). https:\/\/doi.org\/10.14279\/tuj.eceasst.76.1070","DOI":"10.14279\/tuj.eceasst.76.1070"},{"key":"1_CR18","unstructured":"Kamburjan, E., Scaletta, M., Rollshausen, N.: Crowbar: behavioral symbolic execution for deductive verification of active objects. CoRR abs\/2102.10127 (2021). https:\/\/arxiv.org\/abs\/2102.10127"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Manolios, P., Vroon, D.: Integrating static analysis and general-purpose theorem proving for termination analysis. In: Osterweil, L.J., Rombach, H.D., Soffa, M.L. (eds.) 28th International Conference on Software Engineering (ICSE 2006), pp. 873\u2013876. ACM (2006). https:\/\/doi.org\/10.1145\/1134285.1134438","DOI":"10.1145\/1134285.1134438"},{"key":"1_CR20","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-540-88479-8_23","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"L Quan","year":"2008","unstructured":"Quan, L., Zongyan, Q., Liu, Z.: Formal use of design patterns and refactoring. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 323\u2013338. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88479-8_23"},{"issue":"2","key":"1_CR21","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1109\/TSE.2012.19","volume":"39","author":"G Soares","year":"2013","unstructured":"Soares, G., Gheyi, R., Massoni, T.: Automated behavioral testing of refactoring engines. IEEE Trans. Softw. Eng. 39(2), 147\u2013162 (2013). https:\/\/doi.org\/10.1109\/TSE.2012.19","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-030-30942-8_20","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"D Steinh\u00f6fel","year":"2019","unstructured":"Steinh\u00f6fel, D., H\u00e4hnle, R.: Abstract execution. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 319\u2013336. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_20"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-030-61470-6_9","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles","author":"V Stolz","year":"2020","unstructured":"Stolz, V., Pun, V.K.I., Gheyi, R.: Refactoring and active object languages. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12477, pp. 138\u2013158. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61470-6_9"}],"container-title":["Lecture Notes in Computer Science","The Logic of Software. A Tasting Menu of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-08166-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:37:47Z","timestamp":1656891467000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-08166-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031081651","9783031081668"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-08166-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"4 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}