{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T07:30:00Z","timestamp":1775028600274,"version":"3.50.1"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,5,13]],"date-time":"2012-05-13T00:00:00Z","timestamp":1336867200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2013,6]]},"DOI":"10.1007\/s10626-012-0139-x","type":"journal-article","created":{"date-parts":[[2012,5,12]],"date-time":"2012-05-12T02:15:03Z","timestamp":1336788903000},"page":"157-195","source":"Crossref","is-referenced-by-count":33,"title":["Concurrency bugs in multithreaded software: modeling and analysis using Petri nets"],"prefix":"10.1007","volume":"23","author":[{"given":"Hongwei","family":"Liao","sequence":"first","affiliation":[]},{"given":"Yin","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Hyoun Kyu","family":"Cho","sequence":"additional","affiliation":[]},{"given":"Jason","family":"Stanley","sequence":"additional","affiliation":[]},{"given":"Terence","family":"Kelly","sequence":"additional","affiliation":[]},{"given":"St\u00e9phane","family":"Lafortune","sequence":"additional","affiliation":[]},{"given":"Scott","family":"Mahlke","sequence":"additional","affiliation":[]},{"given":"Spyros","family":"Reveliotis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,5,13]]},"reference":[{"key":"139_CR1","unstructured":"Allen LV (2010) Verification and anomaly detection for event-based control of manufacturing systems. PhD thesis, University of Michigan"},{"key":"139_CR2","doi-asserted-by":"crossref","unstructured":"Auer A, Dingel J, Rudie K (2009) Concurrency control generation for dynamic threads using discrete-event systems. In: Proc. Allerton conference on communication, control and computing","DOI":"10.1109\/ALLERTON.2009.5394896"},{"issue":"4","key":"139_CR3","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1109\/81.285680","volume":"41","author":"ER Boer","year":"1994","unstructured":"Boer ER, Murata T (1994) Generating basis siphons and traps of Petri nets using the sign incidence matrix. IEEE Trans Circuits Syst\u2014I 41(4):266\u2013271","journal-title":"IEEE Trans Circuits Syst\u2014I"},{"key":"139_CR4","doi-asserted-by":"crossref","unstructured":"Cano EE, Rovetto CA, Colom JM (2010) An algorithm to compute the minimal siphons in S 4 PR nets. In: Proc. international workshop on discrete event systems, pp 18\u201323","DOI":"10.3182\/20100830-3-DE-4013.00005"},{"key":"139_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-68612-7","volume-title":"Introduction to discrete event systems","author":"CG Cassandras","year":"2008","unstructured":"Cassandras CG, Lafortune S (2008) Introduction to discrete event systems, 2nd edn. Springer, Boston","edition":"2"},{"issue":"6","key":"139_CR6","doi-asserted-by":"crossref","first-page":"793","DOI":"10.1109\/70.650158","volume":"13","author":"F Chu","year":"1997","unstructured":"Chu F, Xie XL (1997) Deadlock analysis of Petri nets using siphons and mathematical programming. IEEE Trans Robot Autom 13(6):793\u2013804","journal-title":"IEEE Trans Robot Autom"},{"key":"139_CR7","doi-asserted-by":"crossref","unstructured":"Delaval G, Marchand H, Rutten E (2010) Contracts for modular discrete controller synthesis. In: Proc. ACM conference on languages, compilers and tools for embedded systems","DOI":"10.1145\/1755888.1755898"},{"key":"139_CR8","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/978-1-4612-5695-3_54","volume-title":"Selected Writings on Computing: A Personal Perspective","author":"EW Dijkstra","year":"1982","unstructured":"Dijkstra EW (1982) The mathematics behind the Banker\u2019s Algorithm. In: Selected Writings on Computing: A Personal Perspective. Springer-Verlag, New York, pp 308\u2013312"},{"key":"139_CR9","doi-asserted-by":"crossref","unstructured":"Dragert C, Dingel J, Rudie K (2008) Generation of concurrency control code using discrete-event systems theory. In: Proc. ACM international symposium on foundations of software engineering","DOI":"10.1145\/1453101.1453122"},{"key":"139_CR10","doi-asserted-by":"crossref","unstructured":"Engler D, Ashcraft K (2003) RacerX: effective, static detection of race conditions and deadlocks. In: Proc. the 19th ACM symposium on operating systems principles","DOI":"10.1145\/945445.945468"},{"issue":"2","key":"139_CR11","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1109\/70.370500","volume":"11","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 Trans Robot Autom 11(2):173\u2013184","journal-title":"IEEE Trans Robot Autom"},{"issue":"4","key":"139_CR12","doi-asserted-by":"crossref","first-page":"621","DOI":"10.1109\/TRA.2002.801048","volume":"18","author":"J Ezpeleta","year":"2002","unstructured":"Ezpeleta J, Garc\u00eda-Vall\u00e9s F, Colom JM (2002) A banker\u2019s solution for deadlock avoidance in FMS with flexible routing and multiresource states. IEEE Trans Robot Autom 18(4):621\u2013625","journal-title":"IEEE Trans Robot Autom"},{"key":"139_CR13","doi-asserted-by":"crossref","unstructured":"Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB, Stata R (2002) Extended static checking for Java. In: Proc. the ACM SIGPLAN 2002 conference on programming language design and implementation","DOI":"10.1145\/512529.512558"},{"key":"139_CR14","doi-asserted-by":"crossref","unstructured":"Gamatie A, Yu H, Delaval G, Rutten E (2009) A case study on controller synthesis for data-intensive embedded system. In: Proc. international conference on embedded software and systems","DOI":"10.1109\/ICESS.2009.12"},{"key":"139_CR15","unstructured":"Giua A (1992) Petri nets as discrete event models for supervisory control. PhD thesis, Rensselaer Polytechnic Institute"},{"key":"139_CR16","unstructured":"Gurobi (2010) Gurobi optimizer. http:\/\/www.gurobi.com\/"},{"key":"139_CR17","volume-title":"Introduction to automata theory, languages, and computation","author":"JE Hopcroft","year":"2006","unstructured":"Hopcroft JE, Motwani R, Ullman JD (2006) Introduction to automata theory, languages, and computation, 3rd edn. Addison Wesley","edition":"3"},{"key":"139_CR18","volume-title":"Supervisory control of concurrent systems: a Petri net structural approach","author":"MV Iordache","year":"2006","unstructured":"Iordache MV, Antsaklis PJ (2006) Supervisory control of concurrent systems: a Petri net structural approach. Birkh\u00e4user, Boston"},{"key":"139_CR19","doi-asserted-by":"crossref","unstructured":"Iordache MV, Antsaklis PJ (2009) Petri nets and programming: a survey. In: Proc. 2009 American control conference, pp 4994\u20134999","DOI":"10.1109\/ACC.2009.5159987"},{"key":"139_CR20","unstructured":"Iordache MV, Antsaklis PJ (2010) Concurrent program synthesis based on supervisory control. In: Proc. 2010 American control conference, pp 3378\u20133383"},{"issue":"5","key":"139_CR21","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1109\/70.964659","volume":"17","author":"M Jeng","year":"2001","unstructured":"Jeng M, Xie X (2001) Modeling and analysis of semiconductor manufacturing systems with degraded behaviors using Petri nets and siphons. IEEE Trans Robot Autom 17(5):576\u2013588","journal-title":"IEEE Trans Robot Autom"},{"issue":"5","key":"139_CR22","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1023\/A:1019917329895","volume":"35","author":"KM Kavi","year":"2002","unstructured":"Kavi KM, Moshtaghi A, Chen D (2002) Modeling multithreaded applications using Petri nets. Int J Parallel Program 35(5):353\u2013371","journal-title":"Int J Parallel Program"},{"issue":"12","key":"139_CR23","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/MC.2009.391","volume":"42","author":"T Kelly","year":"2009","unstructured":"Kelly T, Wang Y, Lafortune S, Mahlke S (2009) Eliminating concurrency bugs with control engineering. IEEE Computer 42(12):52\u201360","journal-title":"IEEE Computer"},{"issue":"2","key":"139_CR24","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1109\/TSMCC.2007.913920","volume":"38","author":"Z Li","year":"2008","unstructured":"Li Z, Zhou M, Wu N (2008) A survey and comparison of Petri net-based deadlock prevention policies for flexible manufacturing systems. IEEE Trans Syst Man Cybern Part C 38(2):173\u2013188","journal-title":"IEEE Trans Syst Man Cybern Part C"},{"key":"139_CR25","doi-asserted-by":"crossref","unstructured":"Liao H, Lafortune S, Reveliotis S, Wang Y, Mahlke S (2010) Synthesis of maximally-permissive liveness-enforcing control policies for Gadara Petri nets. In: Proc. the 49th IEEE conference on decision and control","DOI":"10.1109\/CDC.2010.5716934"},{"key":"139_CR26","doi-asserted-by":"crossref","unstructured":"Liao H, Stanley J, Wang Y, Lafortune S, Reveliotis S, Mahlke S (2011) Deadlock-avoidance control of multithreaded software: an efficient siphon-based algorithm for Gadara Petri nets. In: Proc. the 50th IEEE conference on decision and control","DOI":"10.1109\/CDC.2011.6160535"},{"key":"139_CR27","unstructured":"Liu C, Kondratyev A, Watanabe Y, Desel J, Sangiovanni-Vincentelli A (2006) Schedulability analysis of Petri nets based on structural properties. In: Proc. international conference on application of concurrency to system design"},{"issue":"4","key":"139_CR28","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4):541\u2013580","journal-title":"Proc IEEE"},{"issue":"3","key":"139_CR29","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1109\/32.21759","volume":"15","author":"T Murata","year":"1989","unstructured":"Murata T, Shenker B, Shatz SM (1989) Detection of Ada static deadlocks using Petri net invariants. IEEE Trans Softw Eng 15(3):314\u2013326","journal-title":"IEEE Trans Softw Eng"},{"key":"139_CR30","unstructured":"Musuvathi M, Qadeer S, Ball T, Basler G, Nainar PA, Neamtiu I (2008) Finding and reproducing Heisenbugs in concurrent programs. In: Proc. the 8th USENIX symposium on operating systems design and implementation"},{"key":"139_CR31","doi-asserted-by":"crossref","unstructured":"Nazeem A, Reveliotis S, Wang Y, Lafortune S (2010) Optimal deadlock avoidance for complex resource allocation systems through classification theory. In: Proc. the 10th international workshop on discrete event systems","DOI":"10.3182\/20100830-3-DE-4013.00045"},{"issue":"8","key":"139_CR32","doi-asserted-by":"crossref","first-page":"1818","DOI":"10.1109\/TAC.2010.2095612","volume":"56","author":"A Nazeem","year":"2011","unstructured":"Nazeem A, Reveliotis S, Wang Y, Lafortune S (2011) Designing compact and maximally permissive deadlock avoidance policies for complex resource allocation systems through classification theory: the linear case. IEEE Trans Autom Control 56(8):1818\u20131833","journal-title":"IEEE Trans Autom Control"},{"key":"139_CR33","doi-asserted-by":"crossref","unstructured":"Nir-Buchbinder Y, Tzoref R, Ur S (2008) Deadlocks: From exhibiting to healing. In: Proc. workshop on runtime verification","DOI":"10.1007\/978-3-540-89247-2_7"},{"key":"139_CR34","doi-asserted-by":"crossref","unstructured":"Novark G, Berger ED, Zorn BG (2007) Exterminator: automatically correcting memory errors with high probability. In: Proc. programming language design and implementation","DOI":"10.1145\/1250734.1250736"},{"issue":"12","key":"139_CR35","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/1409360.1409382","volume":"51","author":"G Novark","year":"2008","unstructured":"Novark G, Berger ED, Zorn BG (2008) Exterminator: automatically correcting memory errors with high probability. Commun ACM 51(12):87\u201395","journal-title":"Commun ACM"},{"issue":"10","key":"139_CR36","doi-asserted-by":"crossref","first-page":"1572","DOI":"10.1109\/9.956052","volume":"46","author":"J Park","year":"2001","unstructured":"Park J, Reveliotis SA (2001) Deadlock avoidance in sequential resource allocation systems with multiple resource acquisitions and flexible routings. IEEE Trans Autom Control 46(10):1572\u20131583","journal-title":"IEEE Trans Autom Control"},{"issue":"2","key":"139_CR37","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1109\/TRA.2002.999651","volume":"18","author":"J Park","year":"2002","unstructured":"Park J, Reveliotis SA (2002) Liveness-enforcing supervision for resource allocation systems with uncontrollable behavior and forbidden states. IEEE Trans Robot Autom 18(2):234\u2013240","journal-title":"IEEE Trans Robot Autom"},{"key":"139_CR38","doi-asserted-by":"crossref","unstructured":"Park S, Lu S, Zhou Y (2009) Ctrigger: exposing atomicity violation bugs from their hiding places. In: Proc. 14th international conference on architecture support for programming languages and operating systems","DOI":"10.1145\/1508244.1508249"},{"issue":"9","key":"139_CR39","doi-asserted-by":"crossref","first-page":"1187","DOI":"10.1109\/TC.2004.67","volume":"53","author":"VV Phoha","year":"2004","unstructured":"Phoha VV, Nadgar AU, Ray A, Phoha S (2004) Supervisory control of software systems. IEEE Trans Comput 53(9):1187\u20131199","journal-title":"IEEE Trans Comput"},{"key":"139_CR40","doi-asserted-by":"crossref","unstructured":"Qin F, Tucek J, Sundaresan J, Zhou Y (2005) Rx: treating bugs as allergies\u2014a safe method to survive software failures. In: Proc. the 20th ACM symposium on operating systems principles, pp 235\u2013248","DOI":"10.1145\/1095810.1095833"},{"key":"139_CR41","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69968-9","volume-title":"Petri nets: an introduction","author":"W Reisig","year":"1985","unstructured":"Reisig W (1985) Petri nets: an introduction. Springer, New York"},{"key":"139_CR42","volume-title":"Real-time management of resource allocation systems: a discrete-event systems approach","author":"SA Reveliotis","year":"2005","unstructured":"Reveliotis SA (2005) Real-time management of resource allocation systems: a discrete-event systems approach. Springer, New York"},{"issue":"7","key":"139_CR43","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1145\/1095408.1095421","volume":"3","author":"H Sutter","year":"2005","unstructured":"Sutter H, Larus J (2005) Software and the concurrency revolution. ACM Queue 3(7):54\u201362","journal-title":"ACM Queue"},{"key":"139_CR44","unstructured":"Wallace C, Jensen P, Soparkar N (1996) Supervisory control of workflow scheduling. In: Proc. international workshop on advanced transaction models and architectures"},{"key":"139_CR45","unstructured":"Wang Y (2009) Software failure avoidance using discrete control theory. PhD thesis, University of Michigan"},{"key":"139_CR46","unstructured":"Wang Y, Kelly T, Kudlur M, Lafortune S, Mahlke SA (2008) Gadara: dynamic deadlock avoidance for multithreaded programs. In: Proc. the 8th USENIX symposium on operating systems design and implementation, pp 281\u2013294"},{"key":"139_CR47","doi-asserted-by":"crossref","unstructured":"Wang Y, Lafortune S, Kelly T, Kudlur M, Mahlke S (2009a) The theory of deadlock avoidance via discrete control. In: Proc. the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 252\u2013263","DOI":"10.1145\/1480881.1480913"},{"key":"139_CR48","doi-asserted-by":"crossref","unstructured":"Wang Y, Liao H, Reveliotis S, Kelly T, Mahlke S, Lafortune S (2009b) Gadara nets: Modeling and analyzing lock allocation for deadlock avoidance in multithreaded software. In: Proc. the 48th IEEE conference on decision and control, pp 4971\u20134976","DOI":"10.1109\/CDC.2009.5399950"},{"key":"139_CR49","doi-asserted-by":"crossref","unstructured":"Wang Y, Cho HK, Liao H, Nazeem A, Kelly TP, Lafortune S, Mahlke S, Reveliotis S (2010) Supervisory control of software execution for failure avoidance: experience from the Gadara project. In: Proc. international workshop on discrete event systems","DOI":"10.3182\/20100830-3-DE-4013.00044"},{"issue":"1","key":"139_CR50","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/0005-1098(95)00103-4","volume":"32","author":"K Yamalidou","year":"1996","unstructured":"Yamalidou K, Moody J, Lemmon M, Antsaklis P (1996) Feedback control of Petri nets based on place invariants. Automatica 32(1):15\u201328","journal-title":"Automatica"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-012-0139-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-012-0139-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-012-0139-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T12:24:56Z","timestamp":1561724696000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-012-0139-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5,13]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["139"],"URL":"https:\/\/doi.org\/10.1007\/s10626-012-0139-x","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,5,13]]}}}