{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,3,8]],"date-time":"2023-03-08T17:30:09Z","timestamp":1678296609020},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2010,6,11]],"date-time":"2010-06-11T00:00:00Z","timestamp":1276214400000},"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":[[2010,9]]},"DOI":"10.1007\/s10703-010-0096-7","type":"journal-article","created":{"date-parts":[[2010,6,10]],"date-time":"2010-06-10T09:16:12Z","timestamp":1276161372000},"page":"223-245","source":"Crossref","is-referenced-by-count":9,"title":["Context-aware counter abstraction"],"prefix":"10.1007","volume":"36","author":[{"given":"G\u00e9rard","family":"Basler","sequence":"first","affiliation":[]},{"given":"Michele","family":"Mazzucchi","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Wahl","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,6,11]]},"reference":[{"key":"96_CR1","doi-asserted-by":"crossref","unstructured":"Ball\u00a0T, Rajamani\u00a0SK (2000) Bebop: a symbolic model checker for Boolean programs. In: SPIN, pp\u00a0113\u2013130","DOI":"10.1007\/10722468_7"},{"key":"96_CR2","doi-asserted-by":"crossref","unstructured":"Ball\u00a0T, Rajamani\u00a0SK (2002) The SLAM project: debugging system software via static analysis. In: POPL, pp\u00a01\u20133","DOI":"10.1145\/503272.503274"},{"key":"96_CR3","doi-asserted-by":"crossref","unstructured":"Ball\u00a0T, Chaki\u00a0S, Rajamani\u00a0SK (2001) Parameterized verification of multithreaded software libraries. In: TACAS, pp\u00a0158\u2013173","DOI":"10.1007\/3-540-45319-9_12"},{"key":"96_CR4","doi-asserted-by":"crossref","unstructured":"Ball\u00a0T, Bounimova\u00a0E, Cook\u00a0B, Levin\u00a0V, Lichtenberg\u00a0J, McGarvey\u00a0C, Ondrusek\u00a0B, Rajamani\u00a0SK, Ustuner\u00a0A (2006) Thorough static analysis of device drivers. In: EuroSys, pp\u00a073\u201385","DOI":"10.1145\/1217935.1217943"},{"issue":"1\u20132","key":"96_CR5","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/s10703-005-2246-x","volume":"27","author":"S Barner","year":"2005","unstructured":"Barner\u00a0S, Grumberg\u00a0O (2005) Combining symmetry reduction and under-approximation for symbolic Model Checking. Form Methods Syst Des 27(1\u20132):29\u201366","journal-title":"Form Methods Syst Des"},{"key":"96_CR6","doi-asserted-by":"crossref","unstructured":"Basler\u00a0G, Mazzucchi\u00a0M, Wahl\u00a0T, Kroening\u00a0D (2009) Symbolic counter abstraction for concurrent software. In: CAV, pp\u00a064\u201378","DOI":"10.1007\/978-3-642-02658-4_9"},{"issue":"1","key":"96_CR7","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/s100090200074","volume":"4","author":"D Bosnacki","year":"2002","unstructured":"Bosnacki\u00a0D, Dams\u00a0D, Holenderski\u00a0L (2002) Symmetric spin. Int J Softw Tools Technol Transf 4(1):92\u2013106","journal-title":"Int J Softw Tools Technol Transf"},{"issue":"1\/2","key":"96_CR8","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke\u00a0EM, Jha\u00a0S, Enders\u00a0R, Filkorn\u00a0T (1996) Exploiting symmetry in temporal logic Model Checking. Form Methods Syst Des 9(1\/2):77\u2013104","journal-title":"Form Methods Syst Des"},{"key":"96_CR9","unstructured":"Clarke\u00a0EM, Kroening\u00a0D, Sharygina\u00a0N, Yorav\u00a0K (2005) SATABS: SAT-based predicate abstraction for ANSI-C. In: TACAS, pp\u00a0570\u2013574"},{"key":"96_CR10","unstructured":"Cook\u00a0B, Kroening\u00a0D, Sharygina\u00a0N (2005) Symbolic Model Checking for asynchronous Boolean programs. In: SPIN, pp\u00a075\u201390"},{"issue":"13","key":"96_CR11","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.tcs.2007.07.050","volume":"388","author":"B Cook","year":"2007","unstructured":"Cook\u00a0B, Kroening\u00a0D, Sharygina\u00a0N (2007) Verification of Boolean programs with unbounded thread creation. Theor Comput Sci 388(13):227\u2013242","journal-title":"Theor Comput Sci"},{"key":"96_CR12","doi-asserted-by":"crossref","unstructured":"Delzanno\u00a0G (2000) Automatic verification of parameterized cache coherence protocols. In: CAV, pp\u00a053\u201368","DOI":"10.1007\/10722167_8"},{"key":"96_CR13","unstructured":"Donaldson\u00a0AF, Miller\u00a0A (2006) Exact and approximate strategies for symmetry reduction in model checking. In: FM, pp\u00a0541\u2013556"},{"key":"96_CR14","doi-asserted-by":"crossref","unstructured":"Donaldson\u00a0AF, Miller\u00a0A (2006) Symmetry reduction for probabilistic Model Checking using generic representatives. In: ATVA, pp\u00a09\u201323","DOI":"10.1007\/11901914_4"},{"key":"96_CR15","doi-asserted-by":"crossref","unstructured":"Donaldson\u00a0A, Miller\u00a0A, Parker\u00a0D (2009) Language-level symmetry reduction for probabilistic Model Checking. In: QEST, pp\u00a0289\u2013298","DOI":"10.1109\/QEST.2009.21"},{"issue":"1\/2","key":"96_CR16","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"EA Emerson","year":"1996","unstructured":"Emerson\u00a0EA, Sistla\u00a0AP (1996) Symmetry and Model Checking. Form Methods Syst Des 9(1\/2):105\u2013131","journal-title":"Form Methods Syst Des"},{"key":"96_CR17","unstructured":"Emerson\u00a0EA, Trefler\u00a0RJ (1999) From asymmetry to full symmetry: new techniques for symmetry reduction in Model Checking. In: CHARME, pp\u00a0142\u2013156"},{"key":"96_CR18","doi-asserted-by":"crossref","unstructured":"Emerson\u00a0EA, Wahl\u00a0T (2005) Dynamic symmetry reduction. In: TACAS, pp\u00a0382\u2013396","DOI":"10.1007\/978-3-540-31980-1_25"},{"key":"96_CR19","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1016\/j.entcs.2005.03.019","volume":"130","author":"EA Emerson","year":"2005","unstructured":"Emerson\u00a0EA, Wahl\u00a0T (2005) Efficient reduction techniques for systems with many components. Electron Notes Theor Comput Sci 130:379\u2013399","journal-title":"Electron Notes Theor Comput Sci"},{"key":"96_CR20","doi-asserted-by":"crossref","unstructured":"Emerson\u00a0EA, Jha\u00a0S, Peled\u00a0D (1997) Combining partial order and symmetry reductions. In: TACAS, pp\u00a019\u201334","DOI":"10.1007\/BFb0035378"},{"key":"96_CR21","doi-asserted-by":"crossref","unstructured":"Emerson\u00a0EA, Havlicek\u00a0J, Trefler\u00a0RJ (2000) Virtual symmetry reduction. In: LICS, pp\u00a0121\u2013131","DOI":"10.1109\/LICS.2000.855761"},{"key":"96_CR22","doi-asserted-by":"crossref","unstructured":"Flanagan\u00a0C, Godefroid\u00a0P (2005) Dynamic partial-order reduction for Model Checking software. In: POPL, pp\u00a0110\u2013121","DOI":"10.1145\/1040305.1040315"},{"key":"96_CR23","doi-asserted-by":"crossref","unstructured":"Graf\u00a0S, Sa\u00efdi\u00a0H (1997) Construction of abstract state graphs with PVS. In: CAV, pp\u00a072\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"96_CR24","doi-asserted-by":"crossref","unstructured":"Henzinger\u00a0TA, Jhala\u00a0R, Majumdar\u00a0R (2004) Race checking by context inference. In: PLDI, pp\u00a01\u201313","DOI":"10.1145\/996841.996844"},{"key":"96_CR25","unstructured":"Holzmann\u00a0GJ, Peled\u00a0D (1994) An improvement in formal verification. In: FORTE, pp\u00a0197\u2013211"},{"key":"96_CR26","volume-title":"Computer-aided verification of coordinating processes: the automata-theoretic approach","author":"RP Kurshan","year":"1994","unstructured":"Kurshan\u00a0RP (1994) Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton"},{"key":"96_CR27","doi-asserted-by":"crossref","unstructured":"Lahiri\u00a0SK, Bryant\u00a0RE, Cook\u00a0B (2003) A symbolic approach to predicate abstraction. In: CAV, pp\u00a0141\u2013153","DOI":"10.1007\/978-3-540-45069-6_15"},{"key":"96_CR28","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"BD Lubachevsky","year":"1984","unstructured":"Lubachevsky\u00a0BD (1984) An approach to automating the verification of compact parallel coordination programs I. Acta Inform 21:125\u2013169","journal-title":"Acta Inform"},{"key":"96_CR29","doi-asserted-by":"crossref","unstructured":"Manevich\u00a0R, Lev-Ami\u00a0T, Sagiv\u00a0M, Ramalingam\u00a0G, Berdine\u00a0J (2008) Heap decomposition for concurrent shape analysis. In: SAS, pp\u00a0363\u2013377","DOI":"10.1007\/978-3-540-69166-2_24"},{"key":"96_CR30","unstructured":"Melton\u00a0R, Dill\u00a0D Mur\u03c6 annotated reference manual, rel. 3.1. http:\/\/verify.stanford.edu\/dill\/murphi.html"},{"key":"96_CR31","unstructured":"Pnueli\u00a0A, Xu\u00a0J, Zuck\u00a0LD (2002) Liveness with (0,1,\u221e)-counter abstraction. In: CAV, pp\u00a0107\u2013122"},{"issue":"8","key":"96_CR32","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/71.406955","volume":"6","author":"F Pong","year":"1995","unstructured":"Pong\u00a0F, Dubois\u00a0M (1995) A new approach for the verification of cache coherence protocols. IEEE Trans Parallel Distrib Syst 6(8):773\u2013787","journal-title":"IEEE Trans Parallel Distrib Syst"},{"key":"96_CR33","unstructured":"Somenzi\u00a0F The CU decision diagram package, release 2.3.1. University of Colorado at Boulder. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"key":"96_CR34","unstructured":"Suwimonteerabuth\u00a0D, Esparza\u00a0J, Schwoon\u00a0S (2008) Symbolic context-bounded analysis of multithreaded java programs. In: SPIN, pp\u00a0270\u2013287"},{"key":"96_CR35","doi-asserted-by":"crossref","unstructured":"Wahl\u00a0T, Blanc\u00a0N, Emerson\u00a0EA (2008) SVISS: symbolic verification of symmetric systems. In: TACAS, pp\u00a0459\u2013462","DOI":"10.1007\/978-3-540-78800-3_34"},{"key":"96_CR36","unstructured":"Wei\u00a0O, Gurfinkel\u00a0A, Chechik\u00a0M (2005) Identification and counter abstraction for full virtual symmetry. In: CHARME, pp\u00a0285\u2013300"},{"key":"96_CR37","doi-asserted-by":"crossref","unstructured":"Witkowski\u00a0T, Blanc\u00a0N, Kroening\u00a0D, Weissenbacher\u00a0G (2007) Model Checking concurrent Linux device drivers. In: ASE, pp\u00a0501\u2013504","DOI":"10.1145\/1321631.1321719"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0096-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-010-0096-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0096-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:05:51Z","timestamp":1559239551000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-010-0096-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,6,11]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,9]]}},"alternative-id":["96"],"URL":"https:\/\/doi.org\/10.1007\/s10703-010-0096-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,6,11]]}}}