{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:03:19Z","timestamp":1743022999050,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319681665"},{"type":"electronic","value":"9783319681672"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-68167-2_1","type":"book-chapter","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T23:50:53Z","timestamp":1506383453000},"page":"3-22","source":"Crossref","is-referenced-by-count":1,"title":["Proving Absence of Starvation by Means of\u00a0Abstract Interpretation and Model Checking"],"prefix":"10.1007","author":[{"given":"Helmut","family":"Seidl","sequence":"first","affiliation":[]},{"given":"Ralf","family":"Vogler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.scico.2015.12.005","volume":"120","author":"G Amato","year":"2016","unstructured":"Amato, G., Scozzari, F., Seidl, H., Apinis, K., Vojdani, V.: Efficiently intertwining widening and narrowing. Sci. Comput. Program. 120, 1\u201324 (2016)","journal-title":"Sci. Comput. Program."},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-35182-2_12","volume-title":"Programming Languages and Systems","author":"K Apinis","year":"2012","unstructured":"Apinis, K., Seidl, H., Vojdani, V.: Side-effecting constraint systems: a swiss army knife for program analysis. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 157\u2013172. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-35182-2_12"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Apinis, K., Seidl, H., Vojdani, V.: How to combine widening and narrowing for non-monotonic systems of equations. In: 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 377\u2013386. ACM (2013)","DOI":"10.1145\/2491956.2462190"},{"issue":"2\u20133","key":"1_CR4","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1561\/2500000002","volume":"2","author":"J Bertrane","year":"2015","unstructured":"Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. Found. Trends Program. Lang. 2(2\u20133), 71\u2013190 (2015)","journal-title":"Found. Trends Program. Lang."},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Bertrane, J., Cousot, P., Cousot, R., J\u00e9r\u00f4me Feret, L.M., Min\u00e9, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. In: AIAA Infotech@Aerospace 2010, number AIAA-2010-3385, pp. 1\u201338. American Institue of Aeronautics and Astronautics, April 2010","DOI":"10.2514\/6.2010-3385"},{"issue":"1","key":"1_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1921532.1921553","volume":"36","author":"J Bertrane","year":"2011","unstructured":"Bertrane, J., Cousot, P., Cousot, R., J\u00e9r\u00f4me Feret, L.M., Min\u00e9, A., Rival, X.: Static analysis by abstract interpretation of embedded critical software. Softw. Eng. Notes 36(1), 1\u20138 (2011)","journal-title":"Softw. Eng. Notes"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Bourke, T., Brun, L., Dagand, P., Leroy, X., Pouzet, M., Rieg, L.: A formally verified compiler for lustre. In: Cohen and Vechev [9], pp. 586\u2013601","DOI":"10.1145\/3062341.3062358"},{"issue":"4","key":"1_CR8","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1007\/s00165-005-0071-z","volume":"17","author":"S Chaki","year":"2005","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: Concurrent software verification with states, events, and deadlocks. Formal Asp. Comput. 17(4), 461\u2013483 (2005)","journal-title":"Formal Asp. Comput."},{"key":"1_CR9","unstructured":"Cohen, A., Vechev, M.T. (eds.): Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18\u201323, 2017. ACM (2017)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: An abstract interpretation framework for termination. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22\u201328, 2012, pp. 245\u2013258. ACM (2012)","DOI":"10.1145\/2103656.2103687"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-642-35861-6_7","volume-title":"Formal Aspects of Component Software","author":"FS Boer de","year":"2013","unstructured":"de Boer, F.S., Bravetti, M., Grabe, I., Lee, M., Steffen, M., Zavattaro, G.: A petri net based analysis of deadlocks for active objects and futures. In: P\u0103s\u0103reanu, C.S., Sala\u00fcn, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 110\u2013127. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35861-6_7"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-540-73370-6_16","volume-title":"Model Checking Software","author":"P C\u00e1mara de la","year":"2007","unstructured":"de la C\u00e1mara, P., del Mar Gallardo, M., Merino, P.: Model extraction for ARINC 653 based avionics software. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 243\u2013262. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73370-6_16"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Engler, D.R., Ashcraft, K.: Racerx: effective, static detection of race conditions and deadlocks. In: Scott, M.L., Peterson, L.L. (eds.) Proceedings of the 19th ACM Symposium on Operating Systems Principles 2003, SOSP 2003, Bolton Landing, NY, USA, October 19\u201322, 2003, pp. 237\u2013252. ACM (2003)","DOI":"10.1145\/945445.945468"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-642-38592-6_19","volume-title":"Formal Techniques for Distributed Systems","author":"AE Flores-Montoya","year":"2013","unstructured":"Flores-Montoya, A.E., Albert, E., Genaim, S.: May-happen-in-parallel based deadlock analysis for concurrent objects. In: Beyer, D., Boreale, M. (eds.) FMOODS\/FORTE -2013. LNCS, vol. 7892, pp. 273\u2013288. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38592-6_19"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-662-53413-7_22","volume-title":"Static Analysis","author":"S Schulze Frielinghaus","year":"2016","unstructured":"Schulze Frielinghaus, S., Seidl, H., Vogler, R.: Enforcing termination of interprocedural analysis. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 447\u2013468. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-53413-7_22"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-319-23506-6_14","volume-title":"Correct System Design","author":"S Hahn","year":"2015","unstructured":"Hahn, S., Reineke, J., Wilhelm, R.: Toward compact abstractions for processor pipelines. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 205\u2013220. Springer, Cham (2015). doi: 10.1007\/978-3-319-23506-6_14"},{"issue":"5","key":"1_CR17","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15\u201317, 2015, pp. 247\u2013259. ACM (2015)","DOI":"10.1145\/2676726.2676966"},{"issue":"1","key":"1_CR19","doi-asserted-by":"crossref","first-page":"2:1","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2:1\u20132:70 (2014)","journal-title":"ACM Trans. Comput. Syst."},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Kroening, D., Tautschnig, M.: CBMC - C Bounded Model Checker, pp. 389\u2013391. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"1_CR21","volume-title":"Programming in the OSEK\/VDX Environment","author":"J Lemieux","year":"2001","unstructured":"Lemieux, J.: Programming in the OSEK\/VDX Environment. CMP Media Inc., USA (2001)"},{"issue":"1","key":"1_CR22","first-page":"5:1","volume":"3","author":"M Lv","year":"2016","unstructured":"Lv, M., Guan, N., Reineke, J., Wilhelm, R., Yi, W.: A survey on static cache analysis for real-time systems. LITES 3(1), 5:1\u20135:48 (2016)","journal-title":"LITES"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","year":"2014","unstructured":"McMillan, K.L., Rival, X. (eds.): VMCAI 2014. LNCS, vol. 8318. Springer, Heidelberg (2014)"},{"issue":"1","key":"1_CR24","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symbol. Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symbol. Comput."},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Relational thread-modular static value analysis by abstract interpretation. In: McMillan and Rival [23], pp. 39\u201358","DOI":"10.1007\/978-3-642-54013-4_3"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Naik, M., Park, C., Sen, K., Gay, D.: Effective static deadlock detection. In: 31st International Conference on Software Engineering, ICSE 2009, May 16\u201324, 2009, Vancouver, Canada, Proceedings, pp. 386\u2013396. IEEE (2009)","DOI":"10.1109\/ICSE.2009.5070538"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-19835-9_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Podelski","year":"2011","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants and transition predicate abstraction for program termination. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 3\u201310. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19835-9_2"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Santhiar, A., Kanade, A.: Static deadlock detection for asynchronous c# programs. In: Cohen and Vechev [9], pp. 292\u2013305","DOI":"10.1145\/3140587.3062361"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Schwarz, M.D., Seidl, H., Vojdani, V., Apinis, K.: Precise analysis of value-dependent synchronization in priority scheduled programs. In: McMillan and Rival [23], pp. 21\u201338","DOI":"10.1007\/978-3-642-54013-4_2"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Schwarz, M.D., Seidl, H., Vojdani, V., Lammich, P., M\u00fcller-Olm, M.: Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011, pp. 93\u2013104. ACM (2011)","DOI":"10.1145\/1926385.1926398"},{"key":"1_CR31","unstructured":"Thompson, S., Brat, G.P., Venet, A.: Software model checking of ARINC-653 flight code with MCP. In: Mu\u00f1oz, C.A. (ed.) Second NASA Formal Methods Symposium - NFM 2010, Proceedings, Washington D.C., USA, April 13\u201315, 2010. NASA Conference Proceedings, vol. NASA\/CP-2010-216215, pp. 171\u2013181 (2010)"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-319-10936-7_19","volume-title":"Static Analysis","author":"C Urban","year":"2014","unstructured":"Urban, C., Min\u00e9, A.: A decision tree abstract domain for proving conditional termination. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 302\u2013318. Springer, Cham (2014). doi: 10.1007\/978-3-319-10936-7_19"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Vojdani, V., Apinis, K., R\u00f5tov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the goblint approach. In: Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering, ASE 2016, pp. 391\u2013402. ACM (2016)","DOI":"10.1145\/2970276.2970337"},{"issue":"1","key":"1_CR34","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1145\/210308.210315","volume":"3","author":"SR Walli","year":"1995","unstructured":"Walli, S.R.: The posix family of standards. StandardView 3(1), 11\u201317 (1995)","journal-title":"StandardView"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-11319-2_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Wilhelm","year":"2010","unstructured":"Wilhelm, R., Altmeyer, S., Burgui\u00e8re, C., Grund, D., Herter, J., Reineke, J., Wachter, B., Wilhelm, S.: Static timing analysis for hard real-time systems. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 3\u201322. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11319-2_3"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/11531142_26","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"A Williams","year":"2005","unstructured":"Williams, A., Thies, W., Ernst, M.D.: Static deadlock detection for java libraries. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 602\u2013629. Springer, Heidelberg (2005). doi: 10.1007\/11531142_26"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-642-23702-7_22","volume-title":"Static Analysis","author":"F Zuleger","year":"2011","unstructured":"Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 280\u2013297. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-23702-7_22"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68167-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T19:37:20Z","timestamp":1570131440000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68167-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319681665","9783319681672"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68167-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}