{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T22:16:38Z","timestamp":1648764998266},"reference-count":3,"publisher":"World Scientific Pub Co Pte Lt","issue":"04","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2006,8]]},"abstract":"<jats:p> We present a new abstraction refinement algorithm to better refine the abstract model for formal property verification. In previous work, refinements are selected either based on a set of counter examples of the current abstract model, as in [5, 6, 7, 8, 9, 20, 21], or independent of any counter examples, as in [18]. We (1) introduce a new controllability analysis that is independent of any particular counter examples, (2) apply a new cooperativeness analysis that extracts information from a particular set of counter examples and (3) combine both to better refine the abstract model. We implemented the algorithm and applied it to verify several real-world designs and properties. We compared the algorithm against the abstraction refinement algorithms in [20] and [21] and the interpolation-based reachability analysis in [15]. The experimental results indicate that the new algorithm outperforms the other three algorithms in terms of runtime, abstraction efficiency (as defined in [20]) and the number of proven properties. <\/jats:p>","DOI":"10.1142\/s0129054106004091","type":"journal-article","created":{"date-parts":[[2006,8,4]],"date-time":"2006-08-04T18:37:04Z","timestamp":1154716624000},"page":"763-774","source":"Crossref","is-referenced-by-count":0,"title":["CONTROLLABILITY AND COOPERATIVENESS ANALYSIS FOR AUTOMATIC ABSTRACTION REFINEMENT"],"prefix":"10.1142","volume":"17","author":[{"given":"FREDDY Y. C.","family":"MANG","sequence":"first","affiliation":[{"name":"Advanced Technology Group, Synopsys, Inc., 1 City Centre Drive, Mississauga, Ontario L5B 1M2, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"PEI-HSIN","family":"HO","sequence":"additional","affiliation":[{"name":"Advanced Technology Group, Synopsys, Inc., 2025 NW Cornelius Pass Rd, Hillsboro, OR 97124, U.S.A."}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"reference":[{"key":"rf12","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011254632723"},{"key":"rf13","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"Kurshan R. P.","year":"1994"},{"key":"rf17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054106004091","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T20:40:21Z","timestamp":1565124021000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054106004091"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,8]]},"references-count":3,"journal-issue":{"issue":"04","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[2006,8]]}},"alternative-id":["10.1142\/S0129054106004091"],"URL":"https:\/\/doi.org\/10.1142\/s0129054106004091","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,8]]}}}