{"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":1775028600774,"version":"3.50.1"},"reference-count":20,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"12","license":[{"start":{"date-parts":[[2015,12,1]],"date-time":"2015-12-01T00:00:00Z","timestamp":1448928000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"NSF","award":["CCF-0819882"],"award-info":[{"award-number":["CCF-0819882"]}]},{"name":"NSF","award":["CCF-1138860"],"award-info":[{"award-number":["CCF-1138860"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Automat. Contr."],"published-print":{"date-parts":[[2015,12]]},"DOI":"10.1109\/tac.2015.2426232","type":"journal-article","created":{"date-parts":[[2015,4,24]],"date-time":"2015-04-24T18:29:43Z","timestamp":1429900183000},"page":"3269-3274","source":"Crossref","is-referenced-by-count":9,"title":["SAT-Based Control of Concurrent Software for Deadlock Avoidance"],"prefix":"10.1109","volume":"60","author":[{"given":"Jason","family":"Stanley","sequence":"first","affiliation":[]},{"given":"Hongwei","family":"Liao","sequence":"additional","affiliation":[]},{"given":"Stephane","family":"Lafortune","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21834-7_13"},{"key":"ref11","author":"liao","year":"2012","journal-title":"Modeling analysis control of a class of resource allocation systems arising in concurrent software"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2012.2230814"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-012-0139-x"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2012.2226034"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30476-0_11"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/12.926158"},{"key":"ref17","first-page":"416","article-title":"Petri net analysis using Boolean manipulation","author":"pastor","year":"0","journal-title":"Proc 15th Int Conf Appl Theory Petri Nets"},{"key":"ref18","author":"reveliotis","year":"2005","journal-title":"Real-Time Management of Resource Allocation Systems A Discrete-Event Systems Approach"},{"key":"ref19","first-page":"281","article-title":"Gadara: Dynamic deadlock avoidance for multithreaded programs","author":"wang","year":"0","journal-title":"Proc USENIX Symp on Operating System Design and Implementation"},{"key":"ref4","first-page":"362","article-title":"A symbolic approach for maximally permissive deadlock avoidance in complex resource allocation systems","author":"fei","year":"0","journal-title":"Proc Int Workshop Discrete Event Syst"},{"key":"ref3","author":"fei","year":"2014","journal-title":"Symbolic supervisory control of resource allocation systems"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ICESS.2009.12"},{"key":"ref5","article-title":"SAT encodings of the at-most-k constraint","author":"frisch","year":"0","journal-title":"Proc Int Workshop Modeling ReformulatingConstraint Satisfication Problems"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2009.5159987"},{"key":"ref7","author":"iordache","year":"2006","journal-title":"Supervisory Control of Concurrent Systems A Petri Net Structural Approach"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453122"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-009-0081-8"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2009.391"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73094-1_5"}],"container-title":["IEEE Transactions on Automatic Control"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9\/7342868\/07094252.pdf?arnumber=7094252","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:46:11Z","timestamp":1642005971000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7094252\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12]]},"references-count":20,"journal-issue":{"issue":"12"},"URL":"https:\/\/doi.org\/10.1109\/tac.2015.2426232","relation":{},"ISSN":["0018-9286","1558-2523"],"issn-type":[{"value":"0018-9286","type":"print"},{"value":"1558-2523","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12]]}}}