{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:26:14Z","timestamp":1746001574181},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,8,16]],"date-time":"2012-08-16T00:00:00Z","timestamp":1345075200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,4]]},"DOI":"10.1007\/s10703-012-0170-4","type":"journal-article","created":{"date-parts":[[2012,8,15]],"date-time":"2012-08-15T09:16:31Z","timestamp":1345022191000},"page":"146-174","source":"Crossref","is-referenced-by-count":9,"title":["Code aware resource management"],"prefix":"10.1007","volume":"42","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"de Alfaro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Faella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vishwanath","family":"Raman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,8,16]]},"reference":[{"issue":"6","key":"170_CR1","doi-asserted-by":"crossref","first-page":"724","DOI":"10.1109\/70.63273","volume":"6","author":"ZA Banaszak","year":"1990","unstructured":"Banaszak ZA, Krogh BH (1990) Deadlock avoidance in flexible manufacturing systems with concurrently competing process flows. IEEE Trans Rob Autom 6(6):724\u2013734","journal-title":"IEEE Trans Rob Autom"},{"issue":"3","key":"170_CR2","doi-asserted-by":"crossref","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem R, Jobstmann B, Piterman N, Pnueli A, Sa\u2019ar Y (2012) Synthesis of reactive(1) designs. J Comput Syst Sci 78(3):911\u2013938","journal-title":"J Comput Syst Sci"},{"issue":"2","key":"170_CR3","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/2076450.2076471","volume":"55","author":"R Bod\u00edk","year":"2012","unstructured":"Bod\u00edk R (2012) Compiling what to how: technical perspective. Commun ACM 55(2):102","journal-title":"Commun ACM"},{"key":"170_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35:677\u2013691","journal-title":"IEEE Transactions on Computers"},{"key":"170_CR5","series-title":"Real-time systems series","volume-title":"Hard real-time computing systems: predictable scheduling algorithms and applications","author":"GC Buttazzo","year":"2004","unstructured":"Buttazzo GC (2004) Hard real-time computing systems: predictable scheduling algorithms and applications. Real-time systems series. Springer, Santa Clara"},{"key":"170_CR6","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-642-22110-1_20","volume-title":"CAV 11: proc of 23rd conf on computer aided verification","author":"P Cern\u00fd","year":"2011","unstructured":"Cern\u00fd P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R (2011) Quantitative synthesis for concurrent programs. In: CAV 11: proc of 23rd conf on computer aided verification, pp 243\u2013259"},{"key":"170_CR7","first-page":"257","volume-title":"TACAS","author":"K Chatterjee","year":"2006","unstructured":"Chatterjee K, Henzinger TA (2006) Finitary winning in omega-regular games. In: TACAS, pp 257\u2013271"},{"key":"170_CR8","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1109\/QEST.2004.1348035","volume-title":"QEST 04: proceedings of the first international conference on quantitative evaluation of systems","author":"K Chatterjee","year":"2004","unstructured":"Chatterjee K, de Alfaro L, Henzinger TA (2004) Trading memory for randomness. In: QEST 04: proceedings of the first international conference on quantitative evaluation of systems. IEEE Comput Soc, New York, pp 206\u2013217"},{"key":"170_CR9","series-title":"Lect notes in comp sci","doi-asserted-by":"crossref","first-page":"878","DOI":"10.1007\/11523468_71","volume-title":"Proc 32nd int colloq aut lang prog","author":"K Chatterjee","year":"2005","unstructured":"Chatterjee K, de Alfaro L, Henzinger TA (2005) The complexity of stochastic rabin and streett games. In: Proc 32nd int colloq aut lang prog. Lect notes in comp sci, vol 3580. Springer, Berlin, pp 878\u2013890"},{"key":"170_CR10","first-page":"34","volume-title":"MFCS","author":"K Chatterjee","year":"2009","unstructured":"Chatterjee K, Henzinger TA, Horn F (2009) Stochastic games with finitary objectives. In: MFCS, pp\u00a034\u201354"},{"key":"170_CR11","series-title":"Lect notes in comp sci","first-page":"52","volume-title":"Proc workshop on logic of programs","author":"EM Clarke","year":"1981","unstructured":"Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc workshop on logic of programs. Lect notes in comp sci, vol 131. Springer, Berlin, pp 52\u201371"},{"key":"170_CR12","unstructured":"de Alfaro L (1997) Formal verification of probabilistic systems. PhD thesis, Stanford University. Technical Report STAN-CS-TR-98-1601"},{"key":"170_CR13","first-page":"564","volume-title":"Proc 39th IEEE symp found of comp sci","author":"L Alfaro de","year":"1998","unstructured":"de Alfaro L, Henzinger TA, Kupferman O (1998) Concurrent reachability games. In: Proc 39th IEEE symp found of comp sci. IEEE Comput Soc, New York, pp 564\u2013575"},{"key":"170_CR14","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/1086228.1086265","volume-title":"EMSOFT 05: 5th intl. ACM conference on embedded software","author":"L Alfaro de","year":"2005","unstructured":"de Alfaro L, Faella M, Majumdar R, Raman V (2005) Code aware resource management. In: EMSOFT 05: 5th intl. ACM conference on embedded software. ACM, New York, pp 191\u2013202"},{"key":"170_CR15","volume-title":"Finite state Markovian decision processes","author":"C Derman","year":"1970","unstructured":"Derman C (1970) Finite state Markovian decision processes. Academic Press, San Diego"},{"issue":"10","key":"170_CR16","doi-asserted-by":"crossref","first-page":"741","DOI":"10.1145\/359842.359854","volume":"20","author":"R Devillers","year":"1977","unstructured":"Devillers R (1977) Game interpretation of the deadlock avoidance problem. Commun ACM 20(10):741\u2013745","journal-title":"Commun ACM"},{"key":"170_CR17","unstructured":"ecos homepage. http:\/\/ecos.sourceware.org\/"},{"key":"170_CR18","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1145\/945445.945468","volume-title":"SOSP 03: symposium on operating systems principles","author":"DR Engler","year":"2003","unstructured":"Engler DR, Ashcraft K (2003) RacerX: effective, static detection of race conditions and deadlocks. In: SOSP 03: symposium on operating systems principles. ACM, New York, pp 237\u2013252"},{"issue":"11","key":"170_CR19","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1109\/70.370500","volume":"2","author":"J Ezpeleta","year":"1995","unstructured":"Ezpeleta J, Colom JM, Mart\u00ednez J (1995) A petri net based deadlock prevention policy for flexible manufacturing systems. IEEE Transactions on Robotics and Automation, N 2(11):173\u2013184","journal-title":"IEEE Transactions on Robotics and Automation, N"},{"key":"170_CR20","volume-title":"Competitive Markov decision processes","author":"J Filar","year":"1997","unstructured":"Filar J, Vrieze K (1997) Competitive Markov decision processes. Springer, Berlin"},{"key":"170_CR21","first-page":"112","volume-title":"ATVA","author":"E Filiot","year":"2010","unstructured":"Filiot E, Jin N, Raskin J-F (2010) Compositional algorithms for ltl synthesis. In: ATVA, pp 112\u2013127"},{"key":"170_CR22","first-page":"225","volume-title":"26th ACM SIGPLAN conf on object-oriented programming, systems, languages, and applications (OOPSLA)","author":"G Golan-Gueta","year":"2011","unstructured":"Golan-Gueta G, Grasso Bronson N, Aiken A, Ramalingam G, Sagiv M, Yahav E (2011) Automatic fine-grain locking using shape properties. In: 26th ACM SIGPLAN conf on object-oriented programming, systems, languages, and applications (OOPSLA), pp 225\u2013242"},{"key":"170_CR23","first-page":"60","volume-title":"Proc 14th ACM symp theory of comp","author":"Y Gurevich","year":"1982","unstructured":"Gurevich Y, Harrington L (1982) Trees, automata, and games. In: Proc 14th ACM symp theory of comp. ACM, New York, pp 60\u201365"},{"key":"170_CR24","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1109\/CIM.1992.639106","volume-title":"Proc of 3rd int conf on comp integrated manufacturing","author":"FS Hsieh","year":"1992","unstructured":"Hsieh FS, Chang SC (1992) Deadlock avoidance controller synthesis for flexible manufacturing systems. In: Proc of 3rd int conf on comp integrated manufacturing, pp 252\u2013261"},{"key":"170_CR25","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1109\/70.988975","volume":"18","author":"MV Iordache","year":"2002","unstructured":"Iordache MV, Moody J, Antsaklis PJ (2002) Synthesis of deadlock prevention supervisors using petri nets. IEEE Trans on Robotics and Automation 18:59\u201368","journal-title":"IEEE Trans on Robotics and Automation"},{"issue":"2","key":"170_CR26","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"RM Karp","year":"1969","unstructured":"Karp RM, Miller RE (1969) Parallel program schemata. J Comput Syst Sci 3(2):147\u2013195","journal-title":"J Comput Syst Sci"},{"key":"170_CR27","first-page":"287","volume-title":"ECRTS","author":"C Kloukinas","year":"2003","unstructured":"Kloukinas C, Yovine S (2003) Synthesis of safe, qos extendible, application specific schedulers for heterogeneous real-time systems. In: ECRTS, pp 287\u2013294"},{"key":"170_CR28","first-page":"274","volume-title":"EMSOFT","author":"C Kloukinas","year":"2003","unstructured":"Kloukinas C, Nakhli C, Yovine S (2003) A methodology and tool support for generating scheduled native code for real-time java applications. In: EMSOFT, pp 274\u2013289"},{"key":"170_CR29","first-page":"111","volume-title":"10th int conf on formal methods in computer-aided design (FMCAD)","author":"M Kuperstein","year":"2010","unstructured":"Kuperstein M, Vechev MT, Yahav E (2010) Automatic inference of memory fences. In: 10th int conf on formal methods in computer-aided design (FMCAD), pp 111\u2013119"},{"key":"170_CR30","volume-title":"Proceedings of conference on compiler construction (CC)","author":"GC Necula","year":"2002","unstructured":"Necula GC, McPeak S, Rahul SP, Weimer W (2002) Intermediate language and tools for analysis and transformation of C programs. In: Proceedings of conference on compiler construction (CC)"},{"key":"170_CR31","volume-title":"Operating system concepts","author":"JL Peterson","year":"1988","unstructured":"Peterson JL, Silberschatz A (1988) Operating system concepts. Addison-Wesley, Reading"},{"key":"170_CR32","first-page":"275","volume-title":"LICS","author":"N Piterman","year":"2006","unstructured":"Piterman N, Pnueli A (2006) Faster solutions of rabin and streett games. In: LICS, pp 275\u2013284"},{"issue":"4","key":"170_CR33","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S Savage","year":"1997","unstructured":"Savage S, Burrows M, Nelson CG, Sobalvarro P, Anderson TA (1997) Eraser: a dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems 15(4):391\u2013411","journal-title":"ACM Transactions on Computer Systems"},{"key":"170_CR34","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1145\/1250734.1250754","volume-title":"PLDI","author":"A Solar-Lezama","year":"2007","unstructured":"Solar-Lezama A, Arnold G, Tancau L, Bod\u00edk R, Saraswat VA, Seshia SA (2007) Sketching stencils. In: PLDI, pp 167\u2013178"},{"key":"170_CR35","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1145\/1375581.1375599","volume-title":"ACM SIGPLAN conf on programming language design and implementation (PLDI)","author":"A Solar-Lezama","year":"2008","unstructured":"Solar-Lezama A, Jones CG, Bod\u00edk R (2008) Sketching concurrent data structures. In: ACM SIGPLAN conf on programming language design and implementation (PLDI), pp 136\u2013148"},{"key":"170_CR36","first-page":"135","volume-title":"Handbook of theoretical computer science","author":"W Thomas","year":"1990","unstructured":"Thomas W (1990) Automata on infinite objects. In: van Leeuwen J (ed) Handbook of theoretical computer science, vol\u00a0B. Elsevier\/North-Holland, Amsterdam, pp 135\u2013191. Chapter 4"},{"issue":"4","key":"170_CR37","doi-asserted-by":"crossref","first-page":"1023","DOI":"10.1145\/322344.322351","volume":"29","author":"M Toshimi","year":"1982","unstructured":"Toshimi M (1982) Deadlock avoidance revisited. J ACM 29(4):1023\u20131048","journal-title":"J ACM"},{"key":"170_CR38","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1145\/945445.945471","volume-title":"SOSP 03: symposium on operating systems principles","author":"JR Behren von","year":"2003","unstructured":"von Behren JR, Condit J, Zhou F, Necula GC, Brewer EA (2003) Capriccio: scalable threads for internet services. In: SOSP 03: symposium on operating systems principles. ACM, New York, pp 268\u2013281"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0170-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0170-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0170-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T16:18:26Z","timestamp":1643213906000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0170-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8,16]]},"references-count":38,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,4]]}},"alternative-id":["170"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0170-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8,16]]}}}