{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T22:41:36Z","timestamp":1775256096348,"version":"3.50.1"},"publisher-location":"Cham","reference-count":70,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319980461","type":"print"},{"value":"9783319980478","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-98047-8_9","type":"book-chapter","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T21:05:49Z","timestamp":1540328749000},"page":"129-146","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards Reliable Concurrent Software"],"prefix":"10.1007","author":[{"given":"Marieke","family":"Huisman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastiaan J. C.","family":"Joosten","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Wolfgang Ahrendt et al. Deductive Software Verification \u2013 The KeY Book Vol. 10001. Lecture Notes in Computer Science. Springer International Publishing, 2016. ISBN: 9783319498126.","DOI":"10.1007\/978-3-319-49812-6"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"A. Amighi, S. Blom, and M. Huisman. \u201cVerCors: A Layered Approach to Practical Verification of Concurrent Software\u201d. In: PDP 2016, pp. 495\u2013503.","DOI":"10.1109\/PDP.2016.107"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Afshin Amighi et al. \u201cVerification of Concurrent Systems with VerCors\u201d. In: Formal Methods for Executable Software Models 14th International School on Formal Methods for the Design of Computer Communication, and Software Systems, SFM 2014, Bertinoro, Italy June 16\u201320, 2014, Advanced Lectures 2014, pp. 172\u2013216.","DOI":"10.1007\/978-3-319-07317-0_5"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"A. Amighi et al. \u201cPermission-based separation logic for multithreaded Java programs\u201d. In: LMCS 11.1 (2015).","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"A. Amighi et al. \u201cThe VerCors Project: Setting Up Basecamp\u201d. In: Programming Languages meets Program Verification (PLPV 2012) ACM Press, 2012, pp. 71\u201382. https:\/\/doi.org\/10.1145\/2103776.2103785","DOI":"10.1145\/2103776.2103785"},{"key":"9_CR6","unstructured":"A. Antonik et al. \u201c20 years of modal and mixed specifications\u201d. In: Bulletin of the EATCS 95 (2008), pp. 94\u2013129."},{"key":"9_CR7","unstructured":"R. Baghdadi et al. \u201cPENCIL: Towards a Platform-Neutral Compute Intermediate Language for DSLs\u201d. In: CoRR abs\/1302.5586 (2013)."},{"key":"9_CR8","unstructured":"G. Barthe et al. \u201cJACK: A Tool for Validation of Security and Behaviour of Java Applications\u201d. In: Formal Methods for Components and Objects (FMCO 2006) Vol. 4709. LNCS. Springer, 2007, pp. 152\u2013174."},{"key":"9_CR9","unstructured":"B. Beckert, R. H\u00e4hnle, and P.H. Schmitt, eds. Verification of Object-Oriented Software: The KeY Approach Vol. 4334. LNCS. Springer, 2007."},{"key":"9_CR10","unstructured":"J. van den Berg and B. Jacobs. \u201cThe LOOP compiler for Java and JML\u201d. In: Tools and Algorithms for the Construction and Analysis of Systems Ed. by T. Margaria and W. Yi. Vol. 2031. LNCS. Springer, 2001, pp. 299\u2013312."},{"key":"9_CR11","unstructured":"S. Blom, S. Darabi, and M. Huisman. \u201cVerification of loop parallelisations\u201d. In: FASE Vol. 9033. LNCS. Springer, 2015, pp. 202\u2013217."},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1016\/j.scico.2014.03.013","volume":"95","author":"Stefan Blom","year":"2014","unstructured":"S. Blom, M. Huisman, and M. Mihelv\u030ci\u0107 \u201cSpecification and Verification of GPGPU programs\u201d. In: Science of Computer Programming 95 (3 2014), pp. 376\u2013388. ISSN: 0167\u20136423.","journal-title":"Science of Computer Programming"},{"key":"9_CR13","unstructured":"S. Blom, M. Huisman, and M. Zaharieva-Stojanovski. \u201cHistory-based verification of functional behaviour of concurrent programs\u201d. In: SEFM. Vol. 9276. LNCS. Springer, 2015, pp. 84\u201398."},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"S. Blom et al \u201cThe VerCors Tool Set: Verification of Parallel and Concurrent Software\u201d. In: iFM Vol. 10510. LNCS. Springer, 2017, pp. 102\u2013110.","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"A.R. Bradley. \u201cSAT-Based Model Checking without Unrolling\u201d. In: Verification, Model Checking and Abstract Interpretation (VMCAI) LNCS. Springer, 2011.","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Marc Brockschmidt et al. \u201cCertifying safety and termination proofs for integer transition systems\u201d. In: International Conference on Automated Deduction Springer. 2017, pp. 454\u2013471.","DOI":"10.1007\/978-3-319-63046-5_28"},{"issue":"1-3","key":"9_CR17","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"Stephen Brookes","year":"2007","unstructured":"S. Brookes. \u201cA Semantics for Concurrent Separation Logic\u201d. In: Theoretical Computer Science 375.1\u20133 (2007), pp. 227\u2013270.","journal-title":"Theoretical Computer Science"},{"key":"9_CR18","unstructured":"Steve Brookes and Peter O\u2019Hearn. \u201cConcurrent Separation Logic\u201d. In: ACM SIGLOG News 3.3 (2016), pp. 47\u201365."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"E. Clarke et al. \u201cCounterexample-Guided Abstraction Refinement\u201d. In: Computer-Aided Verification (CAV) Vol. 1855. LNCS. Springer, 2000.","DOI":"10.1007\/10722167_15"},{"key":"9_CR20","unstructured":"D. Cok and J. R. Kiniry. \u201cESC\/Java2: Uniting ESC\/Java and JML: Progress and issues in building and using ESC\/Java2 and a report on a case study involving the use of ESC\/Java2 to verify portions of an Internet voting tally system\u201d. In: Proceedings, Construction and Analysis of Safe Secure and Interoperable Smart devices (CASSIS\u201904) Workshop Ed. by G. Barthe et al. Vol. 3362. LNCS. Springer, 2005, pp. 108\u2013128."},{"key":"9_CR21","doi-asserted-by":"publisher","first-page":"79","DOI":"10.4204\/EPTCS.149.8","volume":"149","author":"David R. Cok","year":"2014","unstructured":"David Cok. \u201cOpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse\u201d. In: 1st Workshop on Formal Integrated Development Environment, (F-IDE) Ed. by Catherine Dubois, Dimitra Giannakopoulou, and Dominique M\u00e9ry. Vol. 149. EPTCS. 2014, pp. 79\u201392. https:\/\/doi.org\/10.4204\/EPTCS.149.8 . URL: http:\/\/dx.doi.org\/10.4204\/EPTCS.149.8","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"9_CR22","first-page":"247","volume-title":"Lecture Notes in Computer Science","author":"Saeed Darabi","year":"2017","unstructured":"S. Darabi, S.C.C. Blom, and M. Huisman. \u201cA Verification Technique for Deterministic Parallel Programs\u201d. In: NASA Formal Methods (NFM) Ed. by C. Barrett, M. Davies, and T. Kahsai. Vol. 10227. LNCS. 2017, pp. 247\u2013264."},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"S. De Gouw et al. \u201cOpenJDK\u2019s java.utils.Collection.sort() is broken: The good, the bad and the worst case\u201d. In: Proc. 27th Intl. Conf on Computer Aided Verification (CAV), San Francisco Ed. by D. Kroening and C. Pasareanu. Vol. 9206. LNCS. Springer, July 2015, pp. 273\u2013289.","DOI":"10.1007\/978-3-319-21690-4_16"},{"key":"9_CR24","volume-title":"A Discipline of Programming Englewood Cliffs","author":"Edsger W Dijkstra","year":"1976","unstructured":"Edsger W. Dijkstra. A Discipline of Programming Englewood Cliffs, N.J.: Prentice-Hall, Inc., 1976."},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"T. Dinsdale-Young et al. \u201cConcurrent Abstract Predicates\u201d. In: ECOOP Ed. by Theo D\u2019Hondt. Vol. 6183. LNCS. Springer, 2010, pp. 504\u2013528.","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"9_CR26","unstructured":"T. Dinsdale-Young et al. \u201cViews: Compositional Reasoning for Concurrent Programs\u201d. In: POPL\u201913 ACM, 2013, pp. 287\u2013300."},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"J. Dohrau et al. \u201cPermission Inference for Array Programs\u201d. In: Computer Aided Verification (CAV) LNCS. Springer, 2018.","DOI":"10.1007\/978-3-319-96142-2_7"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Manuel Fahndrich et al. \u201cIntegrating a Set of Contract Checking Tools into Visual Studio\u201d. In: Proceedings of the 2012 Second International Workshop on Developing Tools as Plug- ins (TOPI) IEEE, June 2012. URL: https:\/\/wwwmicrosoftcom\/en-us\/research\/publication\/integrating-a-set-of-contract-checking-tools-into-visual-studio\/ .","DOI":"10.1109\/TOPI.2012.6229809"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"P. Ferrara and P. M\u00fcller. \u201cAutomatic inference of access permissions\u201d. In: Proceedings of the 13th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2012) LNCS. Springer, 2012, pp. 202\u2013218.","DOI":"10.1007\/978-3-642-27940-9_14"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"R. W. Floyd. \u201cAssigning Meanings to Programs\u201d. In: Proceedings Symposium on Applied Mathematics 19 (1967), pp. 19\u201331.","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"10","key":"9_CR31","doi-asserted-by":"publisher","first-page":"1019","DOI":"10.1109\/TSE.2015.2431688","volume":"41","author":"Juan P. Galeotti","year":"2015","unstructured":"J.P. Galeotti et al. \u201cInferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking\u201d. In: IEEE Transactions on Software Engineering 41 (10 2015), pp. 1019\u20131037.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9_CR32","unstructured":"Archana Ganapathi and David A. Patterson. \u201cCrash Data Collection: A Windows Case Study.\u201d In: Dependable Systems and Networks (DSN) IEEE Computer Society, Aug. 1, 2005, pp. 280\u2013285. ISBN: 0-7695-2282-3."},{"issue":"4","key":"9_CR33","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1109\/MS.2013.81","volume":"30","author":"Michiel van Genuchten","year":"2013","unstructured":"Michiel van Genuchten and Les Hatton. \u201cMetrics with Impact\u201d. In: IEEE Software 30 (4 July 2013), pp. 99\u2013101.","journal-title":"IEEE Software"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"J\u00fcrgen Giesl et al. \u201cProving termination of programs automatically with AProVE\u201d. In: International Joint Conference on Automated Reasoning Springer. 2014, pp. 184\u2013191.","DOI":"10.1007\/978-3-319-08587-6_13"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"R. H\u00e4hnle and M. Huisman. \u201cDeductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools\u201d. In: Computing and Software Science Vol. 10000. LNCS. 2018.","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Nir Hemed, Noam Rinetzky, and Viktor Vafeiadis. \u201cModular Verification of Concurrency- Aware Linearizability\u201d. In: Symposium on Distributed Computing (DISC) Springer, 2015.","DOI":"10.1007\/978-3-662-48653-5_25"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare. \u201cAn Axiomatic Basis for Computer Programming\u201d. In: Communications of the ACM 12.10 (Oct. 1969), pp. 576\u2013580, 583. URL: http:\/\/doi.acmorg\/10.1145\/363235.363259 .","DOI":"10.1145\/363235.363259"},{"key":"9_CR38","unstructured":"Marieke Huisman. \u201cReasoning about Java Programs in higher order logic with PVS and Isabelle\u201d. IPA Dissertation Series, 2001-03. University of Nijmegen, Holland, Feb 2001. URL: ftp:\/\/ftpsop.inria.fr\/lemme\/Marieke.Huisman\/thesis.ps.gz"},{"key":"9_CR39","unstructured":"B. Jacobs and F. Piessens. The VeriFast program verifier Tech. rep. CW520. Katholieke Universiteit Leuven, 2008."},{"key":"9_CR40","unstructured":"M. Janota. \u201cAssertion-based Loop Invariant Generation\u201d. In: 1st International Workshop on Invariant Generation (WING) 2007."},{"issue":"4","key":"9_CR41","first-page":"596","volume":"5","author":"Cliff B Jones","year":"1983","unstructured":"Cliff B. Jones. \u201cTentative Steps Toward a Development Method for Interfering Programs\u201d. In: 5.4 (1983), pp. 596\u2013619.","journal-title":"In"},{"key":"9_CR42","unstructured":"Sebastiaan JC Joosten, Ren\u00e9 Thiemann, and Akihisa Yamada. \u201cCeTA\u2013Certifying Termination and Complexity Proofs in 2016\u201d. In: 15th International Workshop on Termination Ed. by Aart Middeldorp and Ren\u00e9 Thiemann. 2016."},{"key":"9_CR43","unstructured":"U. Juhasz et al. Viper: A Verification Infrastructure for Permission-Based Reasoning Tech. rep. ETH Zurich, 2014."},{"key":"9_CR44","doi-asserted-by":"crossref","unstructured":"R. Jung et al. \u201cIris: Monoids and invariants as an orthogonal basis for concurrent reasoning\u201d. In: Principles of Programming Languages (POPL) 2015.","DOI":"10.1145\/2676726.2676980"},{"key":"9_CR45","doi-asserted-by":"crossref","unstructured":"R. Krebbers et al. \u201cThe Essence of Higher-Order Concurrent Separation Logic\u201d. In: ESOP Vol. 10201. LNCS. Springer, 2017, pp. 696\u2013723.","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"9_CR46","doi-asserted-by":"crossref","unstructured":"K.G. Larsen and B. Thomsen. \u201cA modal process logic\u201d. In: Logic in Computer Science (LICS) IEEE Computer Society, 1988, pp. 203\u2013210.","DOI":"10.1109\/LICS.1988.5119"},{"key":"9_CR47","doi-asserted-by":"crossref","unstructured":"Francesco Logozzo. \u201cPractical verification for the working programmer with CodeContracts and Abstract Interpretation\u201d. In: Verification, Model Checking and Abstract Interpretation (VMCAI) Springer, 2011.","DOI":"10.1007\/978-3-642-18275-4_3"},{"key":"9_CR48","unstructured":"A. Malkis, A. Podelski, and A. Rybalchenko. \u201cThread-Modular Counterexample-Guided Abstraction Refinement\u201d. In: Static Analysis (SAS) Vol. 6337. LNCS. Springer, 2010."},{"key":"9_CR49","isbn-type":"print","doi-asserted-by":"publisher","first-page":"1523","DOI":"10.1145\/2554850.2555021","volume-title":"29th Annual ACM Symposium on Applied Computing (SAC) Gyeongju","author":"Rivalino Matias","year":"2014","unstructured":"Rivalino Matias et al. \u201cAn Empirical Exploratory Study on Operating System Reliability\u201d. In: 29th Annual ACM Symposium on Applied Computing (SAC) Gyeongju, Republic of Korea: ACM, 2014, pp. 1523\u20131528. ISBN: 978-1-4503-2469-4. https:\/\/doi.org\/10.1145\/2554850.2555021","ISBN":"https:\/\/id.crossref.org\/isbn\/9781450324694"},{"key":"9_CR50","first-page":"63","volume":"2000","author":"J\u00f6rg Meyer and Arnd Poetzsch-Heffter. \u201cAn Architecture for Interactive Program Provers\u201d. In: Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference TACAS 2000 Ed. by Susanne Graf and Michael I. Schwartzbach. Vol","year":"1785","unstructured":"J\u00f6rg Meyer and Arnd Poetzsch-Heffter. \u201cAn Architecture for Interactive Program Provers\u201d. In: Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference TACAS 2000 Ed. by Susanne Graf and Michael I. Schwartzbach. Vol. 1785. Lecture Notes in Computer Science. Springer, 2000, pp. 63\u201377.","journal-title":"Springer"},{"key":"9_CR51","doi-asserted-by":"crossref","unstructured":"P. M\u00fcller, M. Schwerhoff and A.J. Summers. \u201cViper A Verification Infrastructure for Permission-Based Reasoning\u201d. In: VMCAI 2016.","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"9_CR52","doi-asserted-by":"crossref","unstructured":"Aleksandar Nanevski et al. \u201cCommunicating State Transition Systems for Fine-Grained Concurrent Resources\u201d In: European Symposium on Programming (ESOP) 2014, pp. 290\u2013310.","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"9_CR53","unstructured":"P. W. O\u2019Hearn, J. Reynolds, and H. Yang. \u201cLocal Reasoning about Programs that Alter Data Structures\u201d. In: Computer Science Logic Ed. by L. Fribourg. Vol. 2142. LNCS. Paris: Springer, 2001, pp. 1\u201319. https:\/\/doi.org\/10.1007\/3540448020_1"},{"key":"9_CR54","first-page":"268","volume-title":"Principles of Programming Languages Venice","author":"P W O\u2019Hearn","year":"2004","unstructured":"P. W. O\u2019Hearn, H. Yang, and J. C. Reynolds. \u201cSeparation and Information Hiding\u201d. In: Principles of Programming Languages Venice, Italy: ACM Press, 2004, pp. 268\u2013280."},{"issue":"1\u20133","key":"9_CR55","first-page":"271","volume":"375","author":"Peter W O\u2019Hearn","year":"2007","unstructured":"Peter W. O\u2019Hearn. \u201cResources, concurrency and local reasoning\u201d. In: 375.1-3 (2007), pp. 271\u2013307. ISSN: 0304-3975. http:\/\/dx.doi.org\/10.1016\/j.tcs.2006.12.035 .","journal-title":"In"},{"key":"9_CR56","doi-asserted-by":"publisher","first-page":"65","DOI":"10.4204\/EPTCS.211.7","volume":"211","author":"Wytse Oortwijn","year":"2016","unstructured":"W. Oortwijn, S. Blom, and M. Huisman. \u201cFuture-based Static Analysis of Message Passing Programs\u201d. In: PLACES 2016, pp. 65\u201372.","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"9_CR57","doi-asserted-by":"crossref","unstructured":"W. Oortwijn et al. \u201cAn Abstraction Technique for Describing Concurrent Program Be- haviour\u201d. In: VSTTE Vol. 10712. LNCS. 2017, pp. 191\u2013209.","DOI":"10.1007\/978-3-319-72308-2_12"},{"key":"9_CR58","isbn-type":"print","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1145\/566172.566181","volume-title":"2002 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) Roma","author":"Thomas J Ostrand","year":"2002","unstructured":"Thomas J. Ostrand and Elaine J. Weyuker. \u201cThe Distribution of Faults in a Large Industrial Software System\u201d. In: 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) Roma, Italy: ACM, 2002, pp. 55\u201364. ISBN: 1-58113-562-9. https:\/\/doi.org\/10.1145\/566172.566181","ISBN":"https:\/\/id.crossref.org\/isbn\/1581135629"},{"key":"9_CR59","isbn-type":"print","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/1007512.1007524","volume-title":"2004 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISTTA)","author":"Thomas J Ostrand","year":"2004","unstructured":"Thomas J. Ostrand, Elaine J. Weyuker, and Robert M. Bell. \u201cWhere the Bugs Are\u201d. In: 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISTTA). Boston, Massachusetts, USA: ACM, 2004, pp. 86\u201396. ISBN: 1-58113-820-2. https:\/\/doi.org\/10.1145\/1007512.1007524","ISBN":"https:\/\/id.crossref.org\/isbn\/1581138202"},{"issue":"4","key":"9_CR60","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"Susan Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. \u201cAn Axiomatic Proof Technique for Parallel Programs\u201d. In: Acta Informatica Journal 6 (1975), pp. 319\u2013340. https:\/\/doi.org\/10.1007\/BF00268134","journal-title":"Acta Informatica"},{"key":"9_CR61","doi-asserted-by":"crossref","unstructured":"P. da Rocha Pinto, T. Dinsdale-Young, and P. Gardner. \u201cSteps in Modular Specifications for Concurrent Modules\u201d. In: Mathematical Foundations of Programming Semantics (MFPS). 2015.","DOI":"10.1016\/j.entcs.2015.12.002"},{"key":"9_CR62","doi-asserted-by":"crossref","unstructured":"P. da Rocha Pinto, T. Dinsdale-Young, and P. Gardner. \u201cTaDA: A Logic for Time and Data Abstraction\u201d. In: European Conference on Object-Oriented Programming (ECOOP) LNCS. Springer, 2014.","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"9_CR63","unstructured":"I. Sergey, A. Nanevski, and A. Banerjee. \u201cSpecifying and Verifying Concurrent Algorithms with Histories and Subjectivity\u201d. In: ESOP Vol. 9032. LNCS. Springer, 2015, pp. 333\u2013358."},{"key":"9_CR64","unstructured":"J. Shen. \u201cEfficient High Performance Computing on Heterogeneous Platforms\u201d. PhD thesis. Technical University of Delft, 2015."},{"key":"9_CR65","unstructured":"Jan Smans, Bart Jacobs, and Frank Piessens. \u201cVeriFast for Java: A Tutorial\u201d. In: Aliasing in Object-Oriented Programming Ed. by Dave Clarke, Tobias Wrigstad, and James Noble. Vol. 7850. LNCS. Springer, 2013."},{"key":"9_CR66","unstructured":"K. Svendsen and L. Birkedal. \u201cImpredicative Concurrent Abstract Predicates\u201d. In: ESOP Vol. 8410. LNCS. Springer, 2014, pp. 149\u2013168."},{"key":"9_CR67","unstructured":"V. Vafeiadis and M.J. Parkinson. \u201cA Marriage of Rely\/Guarantee and Separation Logic\u201d. In: CONCUR Ed. by Lu\u00eds Caires and Vasco Thudichum Vasconcelos. Vol. 4703. LNCS. Springer, 2007, pp. 256\u2013271."},{"key":"9_CR68","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-14295-6_4","volume-title":"Computer Aided Verification","author":"Maged M. Michael","year":"2010","unstructured":"Viktor Vafeiadis. \u201cAutomatically Proving Linearizability\u201d. In: Computer Aided Verification Ed. by Tayssir Touili, Byron Cook, and Paul Jackson. Vol. 6174. Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2010, pp. 450\u2013464. ISBN: 978-3-642-14294-9. https:\/\/doi.org\/10.1007\/978-3-642-14295-6_4 . URL: http:\/\/dxdoiorg\/10.1007\/978-3-642-142956_40 ."},{"key":"9_CR69","doi-asserted-by":"crossref","unstructured":"M. Zaharieva-Stojanovski. \u201cCloser to Reliable Software: Verifying Functional Behaviour of Concurrent Programs\u201d. PhD thesis. University of Twente, 2015. https:\/\/doi.org\/10.3990\/1.9789036539241 .","DOI":"10.3990\/1.9789036539241"},{"key":"9_CR70","volume-title":"Reasoning about Active Object Programs","author":"J Zeilstra","year":"2016","unstructured":"J. Zeilstra. \u201cReasoning about Active Object Programs\u201d. MA thesis. University of Twente, 2016."}],"container-title":["Principled Software Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98047-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T21:20:41Z","timestamp":1775251241000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98047-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319980461","9783319980478"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98047-8_9","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}