{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:11:42Z","timestamp":1774987902120,"version":"3.50.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,4,25]],"date-time":"2012-04-25T00:00:00Z","timestamp":1335312000000},"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":[[2012,8]]},"DOI":"10.1007\/s10703-012-0155-3","type":"journal-article","created":{"date-parts":[[2012,4,24]],"date-time":"2012-04-24T11:02:55Z","timestamp":1335265375000},"page":"25-44","source":"Crossref","is-referenced-by-count":18,"title":["Counterexample-guided abstraction refinement for symmetric concurrent programs"],"prefix":"10.1007","volume":"41","author":[{"given":"Alastair F.","family":"Donaldson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Kaiser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wahl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,4,25]]},"reference":[{"key":"155_CR1","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1007\/978-3-540-24730-2_30","volume-title":"TACAS","author":"T Ball","year":"2004","unstructured":"Ball T, Cook B, Das S, Rajamani SK (2004) Refining approximations in software predicate abstraction. In: TACAS. Lecture notes in computer science, vol 2988. Springer, Berlin, pp 388\u2013403"},{"key":"155_CR2","first-page":"203","volume-title":"Programming language design and implementation (PLDI)","author":"T Ball","year":"2001","unstructured":"Ball T, Majumdar R, Millstein TD, Rajamani SK (2001) Automatic predicate abstraction of C programs. In: Programming language design and implementation (PLDI), pp 203\u2013213"},{"key":"155_CR3","first-page":"1","volume-title":"Principles of programming languages (POPL)","author":"T Ball","year":"2002","unstructured":"Ball T, Rajamani S (2002) The SLAM project: debugging system software via static analysis. In: Principles of programming languages (POPL), pp 1\u20133"},{"issue":"3","key":"155_CR4","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/s10703-010-0096-7","volume":"36","author":"G Basler","year":"2010","unstructured":"Basler G, Mazzucchi M, Wahl T, Kroening D (2010) Context-aware counter abstraction. Form Methods Syst Des 36(3):223\u2013245","journal-title":"Form Methods Syst Des"},{"key":"155_CR5","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/11691372_22","volume-title":"Tools and algorithms for the construction and analysis of systems (TACAS)","author":"S Chaki","year":"2006","unstructured":"Chaki S, Clarke EM, Kidd N, Reps T, Touili T (2006) Verifying concurrent message-passing C programs with recursive calls. In: Tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science. Springer, Berlin, pp 334\u2013349"},{"key":"155_CR6","volume-title":"Formal methods in computer-aided design (FMCAD)","author":"A Cimatti","year":"2010","unstructured":"Cimatti A, Micheli A, Narasamdya I, Roveri M (2010) Verifying SystemC: a software model checking approach. In: Formal methods in computer-aided design (FMCAD)"},{"issue":"5","key":"155_CR7","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752\u2013794","journal-title":"J ACM"},{"issue":"1\u20133","key":"155_CR8","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.tcs.2007.07.050","volume":"388","author":"B Cook","year":"2007","unstructured":"Cook B, Kroening D, Sharygina N (2007) Verification of Boolean programs with unbounded thread creation. Theor Comput Sci 388(1\u20133):227\u2013242","journal-title":"Theor Comput Sci"},{"key":"155_CR9","volume-title":"Linux device drivers","author":"J Corbet","year":"2005","unstructured":"Corbet J, Rubini A, Kroah-Hartman G (2005) Linux device drivers, 3rd edn. O\u2019Reilly Media, Sebastopol","edition":"3"},{"key":"155_CR10","volume-title":"Logic in computer science (LICS)","author":"S Das","year":"2001","unstructured":"Das S, Dill DL (2001) Successive approximation of abstract transition relations. In: Logic in computer science (LICS)"},{"key":"155_CR11","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1007\/978-3-642-22110-1_28","volume-title":"CAV","author":"AF Donaldson","year":"2011","unstructured":"Donaldson AF, Kaiser A, Kroening D, Wahl T (2011) Symmetry-aware predicate abstraction for shared-variable concurrent programs. In: CAV. Lecture notes in computer science, vol 6806. Springer, Berlin, pp 356\u2013371"},{"key":"155_CR12","unstructured":"Donaldson AF, Kaiser A, Kroening D, Wahl T (2011) Symmetry-aware predicate abstraction for shared-variable concurrent programs (extended technical report). CoRR. arXiv:1102.2330"},{"issue":"3\u20134","key":"155_CR13","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/s10817-008-9107-4","volume":"41","author":"AF Donaldson","year":"2008","unstructured":"Donaldson AF, Miller A (2008) Automatic symmetry detection for Promela. J Autom Reason 41(3\u20134):251\u2013293","journal-title":"J Autom Reason"},{"key":"155_CR14","volume-title":"Model checking of software (SPIN)","author":"C Flanagan","year":"2003","unstructured":"Flanagan C, Qadeer S (2003) Thread-modular model checking. In: Model checking of software (SPIN)"},{"key":"155_CR15","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer-aided verification (CAV)","author":"S Graf","year":"1997","unstructured":"Graf S, Sa\u00efdi H (1997) Construction of abstract state graphs with PVS. In: Computer-aided verification (CAV). Lecture notes in computer science. Springer, Berlin, pp 72\u201383"},{"key":"155_CR16","first-page":"331","volume-title":"POPL","author":"A Gupta","year":"2011","unstructured":"Gupta A, Popeea C, Rybalchenko A (2011) Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL. ACM, New York, pp 331\u2013344"},{"key":"155_CR17","volume-title":"Computer-aided verification (CAV)","author":"A Gupta","year":"2011","unstructured":"Gupta A, Popeea C, Rybalchenko A (2011) Threader: a constraint-based verifier for multi-threaded programs. In: Computer-aided verification (CAV)"},{"key":"155_CR18","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"CAV","author":"T Henzinger","year":"2003","unstructured":"Henzinger T, Jhala R, Majumdar R, Qadeer S (2003) Thread-modular abstraction refinement. In: CAV. Lecture notes in computer science. Springer, Berlin, pp 262\u2013274"},{"key":"155_CR19","first-page":"1","volume-title":"Programming language design and implementation (PLDI)","author":"T Henzinger","year":"2004","unstructured":"Henzinger T, Jhala R, Majumdar R (2004) Race checking by context inference. In: Programming language design and implementation (PLDI), pp 1\u201313"},{"issue":"4","key":"155_CR20","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones CB (1983) Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4):596\u2013619","journal-title":"ACM Trans Program Lang Syst"},{"key":"155_CR21","volume-title":"Computer-aided verification (CAV)","author":"A Kaiser","year":"2010","unstructured":"Kaiser A, Kroening D, Wahl T (2010) Dynamic cutoff detection in parameterized concurrent programs. In: Computer-aided verification (CAV)"},{"key":"155_CR22","volume-title":"Architectural support for programming languages and operating systems (ASPLOS)","author":"S Lu","year":"2008","unstructured":"Lu S, Park S, Seo E, Zhou Y (2008) Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: Architectural support for programming languages and operating systems (ASPLOS)"},{"key":"155_CR23","unstructured":"McKenney P (2007) Using Promela and Spin to verify parallel algorithms. LWN.net, weekly edition"},{"issue":"1","key":"155_CR24","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/103727.103729","volume":"9","author":"J Mellor-Crummey","year":"1991","unstructured":"Mellor-Crummey J, Scott M (1991) Algorithms for scalable synchronization on shared-memory multiprocessors. ACM Trans Comput Syst 9(1):21\u201365","journal-title":"ACM Trans Comput Syst"},{"key":"155_CR25","doi-asserted-by":"crossref","unstructured":"Miller A, Donaldson A, Calder M (2006) Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3)","DOI":"10.1145\/1132960.1132962"},{"key":"155_CR26","unstructured":"Speer Owicki S (1975) Axiomatic proof techniques for parallel programs. PhD thesis, Cornell University"},{"key":"155_CR27","volume-title":"Java concurrency in practice","author":"T Peierls","year":"2005","unstructured":"Peierls T, Goetz B, Bloch J, Bowbeer J, Lea D, Holmes D (2005) Java concurrency in practice. Addison-Wesley, Reading"},{"key":"155_CR28","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"534","DOI":"10.1007\/978-3-642-16901-4_35","volume-title":"ICFEM","author":"N Timm","year":"2010","unstructured":"Timm N, Wehrheim H (2010) On symmetries and spotlights\u2014verifying parameterised systems. In: ICFEM. Lecture notes in computer science. Springer, Berlin, pp 534\u2013548"},{"key":"155_CR29","volume-title":"Computer-aided verification (CAV)","author":"S Torre La","year":"2010","unstructured":"La Torre S, Madhusudan P, Parlato G (2010) Model-checking parameterized concurrent programs using linear interfaces. In: Computer-aided verification (CAV)"},{"issue":"2","key":"155_CR30","doi-asserted-by":"crossref","first-page":"799","DOI":"10.3390\/sym2020799","volume":"2","author":"T Wahl","year":"2010","unstructured":"Wahl T, Donaldson A (2010) Replication and abstraction: symmetry in automated formal verification. Symmetry 2(2):799\u2013847","journal-title":"Symmetry"},{"key":"155_CR31","volume-title":"SPIN","author":"Y Yang","year":"2009","unstructured":"Yang Y, Chen X, Gopalakrishnan G, Wang C (2009) Automatic discovery of transition symmetry in multithreaded programs using dynamic analysis. In: SPIN"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0155-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0155-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0155-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:52Z","timestamp":1559253952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0155-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,25]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["155"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0155-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,4,25]]}}}