{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T01:51:41Z","timestamp":1761789101287},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2013,9,20]],"date-time":"2013-09-20T00:00:00Z","timestamp":1379635200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2014,3]]},"DOI":"10.1007\/s10817-013-9290-9","type":"journal-article","created":{"date-parts":[[2013,9,19]],"date-time":"2013-09-19T07:50:30Z","timestamp":1379577030000},"page":"275-329","source":"Crossref","is-referenced-by-count":2,"title":["On Automation in the Verification of Software Barriers: Experience Report"],"prefix":"10.1007","volume":"52","author":[{"given":"Alexander","family":"Malkis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anindya","family":"Banerjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,9,20]]},"reference":[{"key":"9290_CR1","doi-asserted-by":"crossref","unstructured":"Aiken, A., Gay, D.: Barrier inference. In: MacQueen, D.B., Cardelli, L. (eds.) ACM Symposium on Principles of Programming Languages, pp. 342\u2013354. ACM (1998)","DOI":"10.1145\/268946.268974"},{"key":"9290_CR2","unstructured":"Aldrich, J., Barnett, M., Giannakopoulou, D., Leavens, G.T., Sharygina, N. (eds.): Proceedings of the SAVCBS\u201908Workshop at SIGSOFT 2008\/FSE 16, 9\u201310 November. Technical Report CSTR-08-07 (2008)"},{"key":"9290_CR3","unstructured":"Ayari, A.: System verification tools based on Monadic logics. PhD thesis, University of Freiburg (2003)"},{"key":"9290_CR4","unstructured":"Benten, M.S., Jordan, H.F.: Multiprogramming and the performance of parallel programs. In: Rodrigue, G.H. (ed.) Proceedings of the Third SIAM Conference on Parallel Processing for Scientific Computing, 1\u20134 Dec 1987, pp. 374\u2013383. SIAM, Los Angeles, California, USA (1989)"},{"key":"9290_CR5","unstructured":"Bienia, C.: PARSEC\u2014the Princeton application repository for shared memory computers. http:\/\/parsec.cs.princeton.edu , version 2.1 (2009). Retrieved on 5 Jan 2011"},{"key":"9290_CR6","unstructured":"Braun, P., L\u00f6tzbeyer, H., Slotosch, O.: Quest users guide. Technical report, Technische Universit\u00e4t M\u00fcnchen (2000)"},{"key":"9290_CR7","unstructured":"Brooks III, E.D., Axelrod, T.S., Darmohray, G.A.: The Cerberus multiprocessor simulator. In: Rodrigue, G.H. (ed.) Proceedings of the Third SIAM Conference on Parallel Processing for Scientific Computing, 1\u20134 Dec 1987, pp. 384\u2013390. SIAM, Los Angeles, California, USA (1989)"},{"key":"9290_CR8","unstructured":"Bull, J.M., Davey, R.A., Freeman, R., Graham, P.J., Henty, D.S., Kambites, M.E., Obdrz\u00e1lek, J., Pottage, L., Smith, L.A., Telford, S.D., Westhead, M.D.: The Java Grande benchmark suite. http:\/\/www2.epcc.ed.ac.uk\/computing\/research_activities\/java_grande\/index_1.html (2001). Accessed 5 June 2013"},{"key":"9290_CR9","unstructured":"Burckhardt, S.: Memory model sensitive analysis of concurrent data types. PhD thesis, University of Pennsylvania (2007)"},{"key":"9290_CR10","unstructured":"Celmaster, W.: Implementation of the acceptance-rejection method on parallel processors: a case study in scheduling. In: Rodrigue, G.H. (ed.) Proceedings of the Third SIAM Conference on Parallel Processing for Scientific Computing, 1\u20134 Dec 1987, pp. 131\u2013136. SIAM, Los Angeles, California, USA (1989)"},{"key":"9290_CR11","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC\u2014the verifying C compiler. http:\/\/vcc.codeplex.com (2012). Accessed 7 June 2013"},{"key":"9290_CR12","unstructured":"Cordina, J., Fenech, S., Pace, G.J.: Model checking concurrent assembly algorithms. Technical report, Departments of Computer Science and AI, University of Malta (2007)"},{"key":"9290_CR13","unstructured":"Darmohray, G.A., Brooks III, E.D.: Gaussian techniques on shared memory multiprocessor computers. In: Rodrigue, G.H. (ed.) Proceedings of the Third SIAM Conference on Parallel Processing for Scientific Computing, 1\u20134 Dec 1987, pp. 20\u201326. SIAM, Los Angeles, California, USA (1989)"},{"key":"9290_CR14","unstructured":"Dennis Jr., J.E., Mart\u00ednez, J.M., Zhang, X.: Parallel block triangular decompositions for solving sparse nonlinear systems of equations. In: Dongarra, J., Kennedy, K., Messina, P., Sorensen, D.C., Voigt, R.G. (eds.) PPSC, pp. 168\u2013173. SIAM (1991)"},{"key":"9290_CR15","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Shao, Z., Pierce, B.C. (eds.) ACM Symposium on Principles of Programming Languages, pp. 2\u201315. ACM (2009)","DOI":"10.1145\/1594834.1480885"},{"key":"9290_CR16","doi-asserted-by":"crossref","unstructured":"Friesen, J.: Beginning Java 7. Apress. ISBN 978-1-4302-3909-3 (2011)","DOI":"10.1007\/978-1-4302-3910-9"},{"key":"9290_CR17","doi-asserted-by":"crossref","unstructured":"Gebali, F.: Algorithms and Parallel Computing. John Wiley & Sons, Inc. ISBN 978-0-470-90210-3 (2011)","DOI":"10.1002\/9780470932025"},{"key":"9290_CR18","doi-asserted-by":"crossref","unstructured":"Gupta, R.: The fuzzy barrier: a mechanism for high speed synchronization of processors. In: Emer, J.S. (ed.) Intl. Conference on Architectural Support for Programming Languages and Operating Systems, pp. 54\u201363. ACM Press (1989)","DOI":"10.1145\/70082.68187"},{"key":"9290_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01379320","volume":"17","author":"D Hensgen","year":"1988","unstructured":"Hensgen, D., Finkel, R., Manber, U.: Two algorithms for barrier synchronization. Int. J. Parallel Prog. 17, 1\u201317 (1988)","journal-title":"Int. J. Parallel Prog."},{"key":"9290_CR20","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann (2008)"},{"key":"9290_CR21","doi-asserted-by":"crossref","unstructured":"Hobor, A., Gherghina, C.: Barriers in concurrent separation logic. In: Barthe, G. (ed.) Programming Languages and Systems, European Symposium on Programming. Lecture Notes in Computer Science, vol. 6602, pp. 276\u2013296. Springer (2011)","DOI":"10.1007\/978-3-642-19718-5_15"},{"key":"9290_CR22","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley. http:\/\/www.spinroot.com (2003). Accessed 7 June 2013"},{"issue":"3","key":"9290_CR23","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1007\/s100090050034","volume":"2","author":"GJ Holzmann","year":"1999","unstructured":"Holzmann, G.J., Puri, A.: A minimized automaton representation of reachable states. Intl. J. Softw. Tools Technol. Transfer 2(3), 270\u2013278 (1999)","journal-title":"Intl. J. Softw. Tools Technol. Transfer"},{"key":"9290_CR24","unstructured":"Hsu, H.-M., Peir, J.-K., Haidvogel, D.B.: Performance of an ocean circulation model on LCAP. In: Rodrigue, G.H. (ed.) Proceedings of the Third SIAM Conference on Parallel Processing for Scientific Computing, 1\u20134 Dec 1987, p. 285. SIAM, Los Angeles, California, USA (1989)"},{"key":"9290_CR25","doi-asserted-by":"crossref","unstructured":"Huynh, T.Q., Roychoudhury, A.: A memory model sensitive checker for C#. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp.\u00a0476\u2013491. Springer (2006)","DOI":"10.1007\/11813040_32"},{"key":"9290_CR26","unstructured":"Jacobs, B.: Verified general barriers implementation. http:\/\/people.cs.kuleuven.be\/~bart.jacobs\/verifast\/examples\/barrier.c.html (2010). Retrieved on 7 Feb 2013"},{"key":"9290_CR27","unstructured":"Kuncak, V., Wies, T., Zee, K., Malkis, A., Bouillaguet, C., Nguyen, H.H., Schmitt, P.: Jahob verification system. The tool site is at http:\/\/lara.epfl.ch\/w\/jahob_system . The improved source code is at http:\/\/www4.in.tum.de\/~malkis\/jahob.7z and http:\/\/software.imdea.org\/~alexmalkis\/jahob.7z . Accessed 7 June 2013"},{"key":"9290_CR28","doi-asserted-by":"crossref","unstructured":"Leinenbach, D., Santen, T.: Verifying the Microsoft Hyper-V hypervisor with VCC. In: Cavalcanti, A., Dams, D. (eds.) Formal Methods. Lecture Notes in Computer Science, vol. 5850, pp.\u00a0806\u2013809. Springer (2009)","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"9290_CR29","unstructured":"Leino, K.R.M.: This is Boogie 2. Technical Report KRML 178, Microsoft Research (2008)"},{"key":"9290_CR30","unstructured":"Leino, K.R.M., Moskal, M.: VACID-0: Verification of ample correctness of invariants of data-structures, edition 0. In: Tools & Experiments Workshop (2010)"},{"issue":"3","key":"9290_CR31","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/BF01407956","volume":"19","author":"BD Lubachevsky","year":"1990","unstructured":"Lubachevsky, B.D.: Synchronization barrier and related tools for shared memory parallel programming. Int. J. Parallel Prog. 19(3), 225\u2013250 (1990)","journal-title":"Int. J. Parallel Prog."},{"key":"9290_CR32","unstructured":"Malkis, A., Banerjee, A.: Detailed input and comments on the verification tools applied to software barriers. Available at http:\/\/www4.in.tum.de\/~malkis\/BarrierVerification and http:\/\/software.imdea.org\/~ab\/BarrierVerification (2011). Accessed 7 June 2013"},{"key":"9290_CR33","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"9290_CR34","doi-asserted-by":"crossref","unstructured":"Matlin, O.S., Lusk, E.L., McCune, W.: SPINning parallel systems software. In: Bosnacki, D., Leue, S. (eds.) SPIN. Lecture Notes in Computer Science, vol. 2318, pp. 213\u2013220. Springer (2002)","DOI":"10.1007\/3-540-46017-9_16"},{"key":"9290_CR35","unstructured":"May, J.M.: Parallel I\/O for High-Performace Computing. Academic Press (2001). ISBN 1-55860-664-5"},{"key":"9290_CR36","unstructured":"Mellor-Crummey, J.M., Scott, M.L.: Barriers for the BBN Butterfly 1. ftp:\/\/ftp.cs.rochester.edu\/pub\/packages\/scalable_synch\/locks_and_barriers\/Bfly1.tar.Z . Retrieved on 16 Feb 2013"},{"key":"9290_CR37","unstructured":"Mellor-Crummey, J.M., Scott, M.L.: Barriers for the Sequent Symmetry. ftp:\/\/ftp.cs.rochester.edu\/pub\/packages\/scalable_synch\/locks_and_barriers\/Symmetry.tar.Z . Retrieved on 16 Feb 2013"},{"issue":"1","key":"9290_CR38","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1145\/103727.103729","volume":"9","author":"JM Mellor-Crummey","year":"1991","unstructured":"Mellor-Crummey, J.M., Scott, M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. ACM Trans. Comput. Syst. 9(1), 21\u201365 (1991)","journal-title":"ACM Trans. Comput. Syst."},{"key":"9290_CR39","unstructured":"Microsoft Corp.: .NET framework libraries. http:\/\/referencesource.microsoft.com\/netframework.aspx , version 4, file Barrier.cs (2008). Retrieved on 23 May 2011"},{"key":"9290_CR40","unstructured":"Microsoft Corp.: MSDN barrier documentation. http:\/\/msdn.microsoft.com\/en-us\/library\/system.threading.barrier.aspx , sample C# code (2011). Retrieved on 5 July 2011"},{"key":"9290_CR41","unstructured":"Moskal, M., Schulte, W., Cohen, E., Hillebrand, M.A., Tobies, S.: Verifying C programs: a VCC tutorial, (2012). Retrieved from http:\/\/www.codeplex.com\/Download?ProjectName=VCC&DownloadId=476507 on 23 July 2011"},{"key":"9290_CR42","unstructured":"Nagel, C., Evjen, B., Glynn, J., Watson, K., Skinner, M.: Professional C# 2012 and .NET 4.5. John Wiley & Sons, Inc. (2012). ISBN 978-1-1183-1442-5"},{"key":"9290_CR43","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR: FLoC\u201906 Workshop on Empirically Successful Computerized Reasoning. CEUR Workshop Proceedings, vol.\u00a0192, pp. 18\u201333. Seattle, WA, USA (2006)"},{"key":"9290_CR44","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1007\/BF02577741","volume":"22","author":"ML Scott","year":"1994","unstructured":"Scott, M.L., Mellor-Crummey, J.M.: Fast, contention-free combining tree barriers for shared-memory multiprocessors. Int. J. Parallel Prog. 22, 449\u2013481 (1994)","journal-title":"Int. J. Parallel Prog."},{"key":"9290_CR45","unstructured":"Scott, M.L., Mellor-Crummey, J.M.: Pseudocode of scalable synchronization. http:\/\/www.cs.rochester.edu\/research\/synchronization\/pseudocode\/ss.html (1994). Retrieved on 23 Feb 2013"},{"key":"9290_CR46","unstructured":"Smit, A.: Verifying a barrier algorithm with a mechanical theorem prover. Master thesis, Faculty of Mathematics and Natural Sciences, University of Groningen (2001)"},{"key":"9290_CR47","doi-asserted-by":"crossref","unstructured":"Suter, P., Steiger, R., Kuncak, V.: Sets with cardinality constraints in satisfiability modulo theories. In: Jhala, R., Schmidt, D.A. (eds.) Intl. Conf. on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 6538, pp. 403\u2013418. Springer (2011)","DOI":"10.1007\/978-3-642-18275-4_28"},{"key":"9290_CR48","doi-asserted-by":"crossref","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) Frontiers of Combining Systems. Lecture Notes in Computer Science, vol. 5749, pp. 366\u2013382. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_23"},{"issue":"4","key":"9290_CR49","first-page":"388","volume":"36","author":"P-C Yew","year":"1987","unstructured":"Yew, P.-C., Tzeng, N.-F., Lawrie, D.H.: Distributing hot-spot addressing in large-scale multiprocessors. IEEE Trans. Comput. 36(4), 388\u2013395 (1987)","journal-title":"IEEE Trans. Comput."},{"key":"9290_CR50","unstructured":"Yu, S., Kowalski, A.D.: A study of parallel numerical algorithms for the solution of the Navier-Stokes equation. In: Dongarra, J., Messina, P., Sorensen, D.C., Voigt, R.G. (eds.) PPSC, pp.\u00a0285\u2013290. SIAM (1989)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9290-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9290-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9290-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,24]],"date-time":"2019-07-24T06:42:08Z","timestamp":1563950528000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9290-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,20]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,3]]}},"alternative-id":["9290"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9290-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9,20]]}}}