{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,5]],"date-time":"2024-07-05T07:44:26Z","timestamp":1720165466431},"reference-count":173,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Systems and Software"],"published-print":{"date-parts":[[2020,1]]},"DOI":"10.1016\/j.jss.2019.110450","type":"journal-article","created":{"date-parts":[[2019,10,21]],"date-time":"2019-10-21T18:45:21Z","timestamp":1571683521000},"page":"110450","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":2,"special_numbering":"C","title":["A survey on the use of access permission-based specifications for program verification"],"prefix":"10.1016","volume":"159","author":[{"given":"Ayesha","family":"Sadiq","sequence":"first","affiliation":[]},{"given":"Yuan-Fang","family":"Li","sequence":"additional","affiliation":[]},{"given":"Sea","family":"Ling","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/j.jss.2019.110450_bib0001","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/1119479.1119480","article-title":"Types for safe locking: static race detection for Java","volume":"28","author":"Abadi","year":"2006","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.jss.2019.110450_bib0002","series-title":"2018 International Conference on Advancements in Computational Sciences (ICACS)","first-page":"1","article-title":"Checking JML-encoded finite state machine properties","author":"Ahmed","year":"2018"},{"key":"10.1016\/j.jss.2019.110450_bib0003","series-title":"Technical Report","article-title":"The Plaid language: Typed core specification","author":"Aldrich","year":"2012"},{"key":"10.1016\/j.jss.2019.110450_bib0004","series-title":"Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion","first-page":"183","article-title":"Plaid: a permission-based programming language","author":"Aldrich","year":"2011"},{"key":"10.1016\/j.jss.2019.110450_bib0005","series-title":"Proceedings of the 24th ACM SIGPLAN Conference Companion on Object Oriented Programming Systems Languages and Applications","first-page":"1015","article-title":"Typestate-oriented Programming","author":"Aldrich","year":"2009"},{"key":"10.1016\/j.jss.2019.110450_bib0006","series-title":"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-20, 2014, Advanced Lectures","first-page":"172","article-title":"Verification of Concurrent Systems with VerCors","author":"Amighi","year":"2014"},{"key":"10.1016\/j.jss.2019.110450_bib0007","series-title":"2016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP)","first-page":"495","article-title":"Vercors: A layered approach to practical verification of concurrent software","author":"Amighi","year":"2016"},{"key":"10.1016\/j.jss.2019.110450_bib0008","series-title":"Programming Languages meets Program Verification (PLPV 2012)","article-title":"The {VerCors} Project: Setting Up Basecamp","author":"Amighi","year":"2012"},{"key":"10.1016\/j.jss.2019.110450_bib0009","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-11(1:2)2015","article-title":"Permission-based separation logic for multithreaded java programs","author":"Amighi","year":"2015","journal-title":"Logical Methods in Computer Science"},{"key":"10.1016\/j.jss.2019.110450_bib0010","series-title":"Behavioral types in programming languages","author":"Ancona","year":"2016"},{"key":"10.1016\/j.jss.2019.110450_bib0011","series-title":"Theorem Proving in Higher Order Logics","first-page":"5","article-title":"Separation Logic for small-step cminor","author":"Appel","year":"2007"},{"key":"10.1016\/j.jss.2019.110450_bib0012","series-title":"Software Reliability Engineering, 2008. ISSRE 2008. 19th International Symposium on","first-page":"37","article-title":"Concurrent contracts for Java in JML","author":"Araujo","year":"2008"},{"key":"10.1016\/j.jss.2019.110450_bib0013","series-title":"Software Testing Verification and Reliability","article-title":"High-level data races","author":"Artho","year":"2003"},{"key":"10.1016\/j.jss.2019.110450_bib0014","series-title":"Formal Methods for Components and Objects","first-page":"364","article-title":"Boogie: A modular reusable verifier for object-oriented programs","author":"Barnett","year":"2006"},{"key":"10.1016\/j.jss.2019.110450_sbref0070a","first-page":"1","author":"Barrett","year":"2010","journal-title":"The SMTLIB Standard Version 2.0,"},{"key":"10.1016\/j.jss.2019.110450_bib0015","series-title":"Verification of object-oriented software: the KeY approach","author":"Beckert","year":"2007"},{"key":"10.1016\/j.jss.2019.110450_bib0016","series-title":"Proceedings of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications","first-page":"737","article-title":"Modular typestate checking in concurrent Java programs","author":"Beckman","year":"2009"},{"key":"10.1016\/j.jss.2019.110450_bib0017","series-title":"Types for Correct Concurrent API Usage, PhD thesis, technical report CMU-ISR-10-131","author":"Beckman","year":"2010"},{"key":"10.1016\/j.jss.2019.110450_bib0018","series-title":"Proceedings of the 23rd ACM SIGPLAN Conference on Object-oriented Programming Systems Languages and Applications","first-page":"227","article-title":"Verifying Correct Usage of Atomic Blocks and Typestate","author":"Beckman","year":"2008"},{"key":"10.1016\/j.jss.2019.110450_bib0019","series-title":"Proceedings of the 25th European Conference on Object-oriented Programming","first-page":"2","article-title":"An Empirical Study of Object Protocols in the Wild","author":"Beckman","year":"2011"},{"key":"10.1016\/j.jss.2019.110450_bib0020","series-title":"Proceedings of the ACM international conference on Object oriented programming systems languages and applications - OOPSLA \u201912","first-page":"113","article-title":"GPUVerify","author":"Betts","year":"2012"},{"key":"10.1016\/j.jss.2019.110450_sbref0021","series-title":"Api Protocol Compliance in Object-oriented Software","author":"Bierhoff","year":"2009"},{"key":"10.1016\/j.jss.2019.110450_bib0022","series-title":"Proceedings of the 10th SIGPLAN symposium on New ideas, new paradigms, and reflections on programming and software","first-page":"19","article-title":"Automated program verification made SYMPLAR: symbolic permissions for lightweight automated reasoning","author":"Bierhoff","year":"2011"},{"key":"10.1016\/j.jss.2019.110450_bib0023","article-title":"Modular typestate checking of aliased objects","volume":"42","author":"Bierhoff","year":"2007"},{"key":"10.1016\/j.jss.2019.110450_bib0024","series-title":"Companion of the 30th International Conference on Software Engineering","first-page":"971","article-title":"PLURAL: Checking Protocol Compliance Under Aliasing","author":"Bierhoff","year":"2008"},{"key":"10.1016\/j.jss.2019.110450_bib0025","series-title":"Proceedings of the 18th ACM SIGSOFT International Symposium on Software Testing and Analysis","article-title":"Polymorphic fractional permission inference","author":"Bierhoff","year":"2009"},{"key":"10.1016\/j.jss.2019.110450_bib0026","series-title":"ECOOP","first-page":"195","article-title":"Practical API Protocol Checking with Access Permissions","author":"Bierhoff","year":"2009"},{"key":"10.1016\/j.jss.2019.110450_bib0027","series-title":"Integrated Formal Methods","first-page":"102","article-title":"The vercors tool set: Verification of parallel and concurrent software","author":"Blom","year":"2017"},{"key":"10.1016\/j.jss.2019.110450_bib0028","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","article-title":"The vercors tool for verification of concurrent programs","author":"Blom","year":"2014"},{"key":"10.1016\/j.jss.2019.110450_bib0029","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1016\/j.scico.2014.03.013","article-title":"Specification and verification of GPGPU programs","volume":"95","author":"Blom","year":"2014","journal-title":"Sci. Comput. Program"},{"issue":"1","key":"10.1016\/j.jss.2019.110450_bib0030","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1145\/1047659.1040327","article-title":"Permission accounting in Separation Logic","volume":"40","author":"Bornat","year":"2005","journal-title":"SIGPLAN Not."},{"key":"10.1016\/j.jss.2019.110450_bib0031","series-title":"Proceedings of the 17th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications","first-page":"211","article-title":"Ownership Types for Safe Programming: Preventing Data Races and Deadlocks","author":"Boyapati","year":"2002"},{"key":"10.1016\/j.jss.2019.110450_bib0032","series-title":"Proceedings of the 16th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications","first-page":"56","article-title":"A Parameterized Type System for Race-free Java Programs","author":"Boyapati","year":"2001"},{"key":"10.1016\/j.jss.2019.110450_bib0033","series-title":"Proceedings of the 10th International Conference on Static Analysis","first-page":"55","article-title":"Checking Interference with Fractional Permissions","author":"Boyland","year":"2003"},{"issue":"5","key":"10.1016\/j.jss.2019.110450_bib0034","doi-asserted-by":"crossref","first-page":"5","DOI":"10.5381\/jot.2006.5.5.a1","article-title":"Why we should not add readonly to Java (yet).","volume":"5","author":"Boyland","year":"2006","journal-title":"The Journal of Object Technology"},{"issue":"6","key":"10.1016\/j.jss.2019.110450_bib0035","doi-asserted-by":"crossref","first-page":"22:1","DOI":"10.1145\/1749608.1749611","article-title":"Semantics of fractional permissions with nesting","volume":"32","author":"Boyland","year":"2010","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.jss.2019.110450_bib0036","series-title":"A Semantics for Concurrent Separation Logic","first-page":"16","author":"Brookes","year":"2004"},{"key":"10.1016\/j.jss.2019.110450_bib0037","series-title":"Programming with POSIX threads","author":"Butenhof","year":"1997"},{"issue":"2\u20133","key":"10.1016\/j.jss.2019.110450_bib0039","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1016\/j.tcs.2008.04.030","article-title":"Spatial-behavioral types for concurrency and resource control in distributed systems","volume":"402","author":"Caires","year":"2008","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.jss.2019.110450_bib0040","series-title":"Proceedings of the 13th International Conference on Concurrency Theory","first-page":"209","article-title":"A Spatial Logic for Concurrency (Part II)","author":"Caires","year":"2002"},{"issue":"2","key":"10.1016\/j.jss.2019.110450_bib0041","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/S0890-5401(03)00137-8","article-title":"A Spatial Logic for concurrency (Part i)","volume":"186","author":"Caires","year":"2003","journal-title":"Inf. Comput."},{"key":"10.1016\/j.jss.2019.110450_bib0042","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","article-title":"Session types as intuitionistic linear propositions","author":"Caires","year":"2010"},{"key":"10.1016\/j.jss.2019.110450_bib0043","series-title":"Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"275","article-title":"The Type Discipline of Behavioral Separation","author":"Caires","year":"2013"},{"issue":"C","key":"10.1016\/j.jss.2019.110450_bib0044","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/j.entcs.2016.03.007","article-title":"An imperative pure calculus","volume":"322","author":"Capriccioli","year":"2016","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"8","key":"10.1016\/j.jss.2019.110450_bib0045","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1109\/TSE.2016.2625248","article-title":"Automatic contract insertion with ccbot","volume":"43","author":"Carr","year":"2017","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/j.jss.2019.110450_bib0046","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1016\/j.scico.2013.01.004","article-title":"A case study on the lightweight verification of a multi-threaded task server","volume":"80","author":"Cata\u00f1o","year":"2014","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.jss.2019.110450_bib0047","series-title":"Proceedings of the 9th International Conference on Principles and Practice of Programming in Java","first-page":"51","article-title":"Habanero-Java: The New Adventures of Old X10","author":"Cav","year":"2011"},{"issue":"6","key":"10.1016\/j.jss.2019.110450_bib0048","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1109\/TSE.2004.22","article-title":"Modular verification of software components in C","volume":"30","author":"Chaki","year":"2004","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/j.jss.2019.110450_bib0049","series-title":"Handbook of Model Checking","first-page":"219","article-title":"BDD-Based Symbolic Model Checking","author":"Chaki","year":"2018"},{"key":"10.1016\/j.jss.2019.110450_bib0050","series-title":"Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"45","article-title":"Types As Models: Model Checking Message-passing Programs","author":"Chaki","year":"2002"},{"key":"10.1016\/j.jss.2019.110450_bib0051","series-title":"External Uniqueness Is Unique Enough","first-page":"176","author":"Clarke","year":"2003"},{"key":"10.1016\/j.jss.2019.110450_bib0052","series-title":"Ownership Types: A Survey","first-page":"15","author":"Clarke","year":"2013"},{"key":"10.1016\/j.jss.2019.110450_bib0053","series-title":"Proceedings of the 5th...","article-title":"Deny Capabilities for Safe, Fast Actors","author":"Clebsch","year":"2015"},{"key":"10.1016\/j.jss.2019.110450_bib0054","series-title":"VCC: A Practical System for Verifying Concurrent C","first-page":"23","author":"Cohen","year":"2009"},{"key":"10.1016\/j.jss.2019.110450_bib0055","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","article-title":"OpenJML: JML for Java 7 by extending OpenJDK","author":"Cok","year":"2011"},{"key":"10.1016\/j.jss.2019.110450_bib0056","series-title":"Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages","first-page":"238","article-title":"Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints","author":"Cousot","year":"1977"},{"key":"10.1016\/j.jss.2019.110450_bib0057","article-title":"Adoption and focus: practical linear types for imperative programming","author":"DeLine","year":"2002","journal-title":"Programming language design and implementation, ACM SIGPLAN"},{"key":"10.1016\/j.jss.2019.110450_bib0058","series-title":"ECOOP 2004 \u2013 Object-Oriented Programming","first-page":"465","article-title":"Typestates for Objects","author":"DeLine","year":"2004"},{"key":"10.1016\/j.jss.2019.110450_bib0059","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","article-title":"A distributed object-oriented language with session types","author":"Dezani-Ciancaglini","year":"2005"},{"key":"10.1016\/j.jss.2019.110450_bib0060","series-title":"Precise Detection of Atomicity Violations","first-page":"8","author":"Dias","year":"2013"},{"key":"10.1016\/j.jss.2019.110450_bib0061","series-title":"Proceedings of the 24th European Conference on Object-oriented Programming","first-page":"504","article-title":"Concurrent Abstract Predicates","author":"Dinsdale-Young","year":"2010"},{"key":"10.1016\/j.jss.2019.110450_bib0062","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","article-title":"A fresh look at separation algebras and share accounting","author":"Dockins","year":"2009"},{"key":"10.1016\/j.jss.2019.110450_bib0063","series-title":"Computer Aided Verification","first-page":"55","article-title":"Permission inference for array programs","author":"Dohrau","year":"2018"},{"issue":"1","key":"10.1016\/j.jss.2019.110450_bib0064","doi-asserted-by":"crossref","first-page":"4:1","DOI":"10.1145\/2160910.2160913","article-title":"A data-centric approach to synchronization","volume":"34","author":"Dolby","year":"2012","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.jss.2019.110450_bib0065","series-title":"Proceedings of the Nineteenth ACM Symposium on Operating Systems Principles","first-page":"237","article-title":"RacerX: Effective, Static Detection of Race Conditions and Deadlocks","author":"Engler","year":"2003"},{"key":"10.1016\/j.jss.2019.110450_bib0066","series-title":"Proceedings of the 2010 International Conference on Formal Verification of Object-oriented Software","first-page":"10","article-title":"Static contract checking with abstract interpretation","author":"F\u00e4hndrich","year":"2011"},{"key":"10.1016\/j.jss.2019.110450_bib0067","series-title":"Verification, Model Checking, and Abstract Interpretation: 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings","first-page":"202","article-title":"Automatic Inference of Access Permissions","author":"Ferrara","year":"2012"},{"key":"10.1016\/j.jss.2019.110450_bib0068","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","article-title":"Why3 - Where programs meet provers","author":"Filli\u00e2tre","year":"2013"},{"issue":"4","key":"10.1016\/j.jss.2019.110450_bib0069","doi-asserted-by":"crossref","first-page":"20:1","DOI":"10.1145\/1377492.1377495","article-title":"Types for atomicity: static checking and inference for Java","volume":"30","author":"Flanagan","year":"2008","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.jss.2019.110450_bib0070","series-title":"Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation - PLDI \u201903","first-page":"338","article-title":"A type and effect system for atomicity","author":"Flanagan","year":"2003"},{"key":"10.1016\/j.jss.2019.110450_bib0071","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","article-title":"Assigning meanings to programs","volume":"19","author":"Floyd","year":"1967","journal-title":"Proceedings of Symposium on Applied Mathematics"},{"issue":"4","key":"10.1016\/j.jss.2019.110450_bib0072","doi-asserted-by":"crossref","first-page":"12:1","DOI":"10.1145\/2629609","article-title":"Foundations of typestate-oriented programming","volume":"36","author":"Garcia","year":"2014","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"10.1016\/j.jss.2019.110450_bib0074","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-11(4:12)2015","article-title":"Modular session types for objects","volume":"11","author":"Gay","year":"2015","journal-title":"Logical Methods in Computer Science"},{"key":"10.1016\/j.jss.2019.110450_bib0075","doi-asserted-by":"crossref","DOI":"10.1017\/S0956796809990268","article-title":"Linear type theory for asynchronous session types","author":"Gay","year":"2010","journal-title":"J. Funct. Program"},{"key":"10.1016\/j.jss.2019.110450_bib0076","series-title":"FM 2011: Formal Methods","first-page":"386","article-title":"Structured specifications for better verification of heap-manipulating programs","author":"Gherghina","year":"2011"},{"key":"10.1016\/j.jss.2019.110450_bib0077","article-title":"Tracing sharing in an imperative pure calculus","volume":"abs\/1803.0","author":"Giannini","year":"2018","journal-title":"CoRR"},{"key":"10.1016\/j.jss.2019.110450_bib0078","series-title":"Proceedings of the 33rd Annual ACM Symposium on Applied Computing","first-page":"1038","article-title":"A Type and Effect System for Uniqueness and Immutability","author":"Giannini","year":"2018"},{"issue":"1","key":"10.1016\/j.jss.2019.110450_bib0079","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.jss.2019.110450_bib0080","series-title":"Proceedings of the ACM international conference on Object oriented programming systems languages and applications - OOPSLA \u201912","article-title":"Uniqueness and reference immutability for safe parallelism","author":"Gordon","year":"2012"},{"issue":"6","key":"10.1016\/j.jss.2019.110450_bib0081","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1145\/1273442.1250765","article-title":"Thread-modular shape analysis","volume":"42","author":"Gotsman","year":"2007","journal-title":"SIGPLAN Not."},{"key":"10.1016\/j.jss.2019.110450_bib0082","series-title":"Technical Report","article-title":"A Programmer-Oriented Approach to Safe Concurrency","author":"Greenhouse","year":"2003"},{"key":"10.1016\/j.jss.2019.110450_bib0083","series-title":"Proceedings of the 24th International Conference on Software Engineering","article-title":"Assuring and evolving concurrent programs: annotations and policy","author":"Greenhouse","year":"2002"},{"key":"10.1016\/j.jss.2019.110450_bib0084","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","article-title":"Reasoning about java\u2019s reentrant locks","author":"Haack","year":"2008"},{"key":"10.1016\/j.jss.2019.110450_bib0085","series-title":"Algebraic Methodology and Software Technology","first-page":"199","article-title":"Separation Logic Contracts for a Java-Like Language with Fork\/Join","author":"Haack","year":"2008"},{"key":"10.1016\/j.jss.2019.110450_bib0086","series-title":"Proceedigns of the 30th International Conference on Software Engineering (ICSE\u2019 08)","article-title":"Dynamic Detection of Atomic-Set-Serializability Violations","author":"Hammer","year":"2008"},{"key":"10.1016\/j.jss.2019.110450_bib0087","series-title":"Proceedings of the 13th Workshop on Formal Techniques for Java-Like Programs","first-page":"1","article-title":"Fractional permissions without the fractions","author":"Heule","year":"2011"},{"key":"10.1016\/j.jss.2019.110450_bib0088","series-title":"International Workshop on Verification, Model Checking, and Abstract Interpretation","first-page":"315","article-title":"Abstract read permissions: Fractional permissions without the fractions","author":"Heule","year":"2013"},{"issue":"10","key":"10.1016\/j.jss.2019.110450_bib0089","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"key":"10.1016\/j.jss.2019.110450_bib0090","series-title":"The Origin of Concurrent Programming","first-page":"231","article-title":"Towards a Theory of Parallel Programming","author":"Hoare","year":"1972"},{"key":"10.1016\/j.jss.2019.110450_bib0091","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1145\/355620.361161","article-title":"Monitors: an operating system structuring concept","volume":"17","author":"Hoare","year":"1974","journal-title":"Commun. ACM"},{"key":"10.1016\/j.jss.2019.110450_bib0092","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","article-title":"Oracle semantics for concurrent separation logic","author":"Hobor","year":"2008"},{"key":"10.1016\/j.jss.2019.110450_bib0093","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-8(2:2)2012","article-title":"Barriers in concurrent separation logic: now with tool support!","author":"Hobor","year":"2012","journal-title":"Logical Methods in Computer Science"},{"key":"10.1016\/j.jss.2019.110450_bib0094","series-title":"Types for Dyadic Interaction","first-page":"509","author":"Honda","year":"1993"},{"key":"10.1016\/j.jss.2019.110450_bib0095","series-title":"Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems","first-page":"122","article-title":"Language Primitives and Type Discipline for Structured Communication-Based Programming","author":"Honda","year":"1998"},{"key":"10.1016\/j.jss.2019.110450_bib0096","series-title":"Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"273","article-title":"Multiparty Asynchronous Session Types","author":"Honda","year":"2008"},{"key":"10.1016\/j.jss.2019.110450_bib0097","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","article-title":"Type-safe eventful sessions in Java","author":"Hu","year":"2010"},{"key":"10.1016\/j.jss.2019.110450_bib0098","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","article-title":"Session-based distributed programming in Java","author":"Hu","year":"2008"},{"key":"10.1016\/j.jss.2019.110450_bib0099","series-title":"Reasoning about Java programs in higher order logic using PVS and Isabelle. PhD Thesis","author":"Huisman","year":"2001"},{"key":"10.1016\/j.jss.2019.110450_bib0100","series-title":"Proceedings - IEEE 14th International Symposium on Parallel and Distributed Computing, ISPDC 2015","article-title":"A symbolic approach to permission accounting for concurrent reasoning","author":"Huisman","year":"2015"},{"issue":"1","key":"10.1016\/j.jss.2019.110450_bib0101","doi-asserted-by":"crossref","first-page":"3:1","DOI":"10.1145\/2873052","article-title":"Foundations of session types and behavioural contracts","volume":"49","author":"H\u00fcttel","year":"2016","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/j.jss.2019.110450_bib0102","series-title":"POPL","article-title":"Resource usage analysis","author":"Igarashi","year":"2001"},{"issue":"2","key":"10.1016\/j.jss.2019.110450_bib0103","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1145\/1057387.1057390","article-title":"Resource usage analysis","volume":"27","author":"Igarashi","year":"2005","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.jss.2019.110450_bib0104","series-title":"Third IEEE International Conference on Software Engineering and Formal Methods (SEFM\u201905)","first-page":"137","article-title":"Safe concurrency for aggregate objects with invariants","author":"Jacobs","year":"2005"},{"key":"10.1016\/j.jss.2019.110450_bib0105","series-title":"Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"271","article-title":"Expressive modular fine-grained concurrency specification","author":"Jacobs","year":"2011"},{"key":"10.1016\/j.jss.2019.110450_bib0106","series-title":"NASA Formal Methods Symposium","first-page":"41","article-title":"VeriFast: A powerful, sound, predictable, fast verifier for C and java","author":"Jacobs","year":"2011"},{"key":"10.1016\/j.jss.2019.110450_bib0107","series-title":"A Quick Tour of the VeriFast Program Verifier","first-page":"304","author":"Jacobs","year":"2010"},{"key":"10.1016\/j.jss.2019.110450_bib0108","series-title":"Programming Languages and Systems","first-page":"377","article-title":"Fictional Separation Logic","author":"Jensen","year":"2012"},{"key":"10.1016\/j.jss.2019.110450_bib0109","series-title":"IFIP Congress","article-title":"Specification and Design of (Parallel) Programs","author":"Jones","year":"1983"},{"key":"10.1016\/j.jss.2019.110450_bib0110","series-title":"Companion Proceedings for the ISSTA\/ECOOP 2018 Workshops","first-page":"40","article-title":"An exercise in verifying sequential programs with vercors","author":"Joosten","year":"2018"},{"key":"10.1016\/j.jss.2019.110450_bib0111","doi-asserted-by":"crossref","DOI":"10.1007\/s10009-011-0197-7","article-title":"Finding concurrency-related bugs using random isolation","author":"Kidd","year":"2011","journal-title":"Int. J. Software Tools Technol. Trans"},{"key":"10.1016\/j.jss.2019.110450_bib0112","series-title":"Proceedings of the 8th international workshop on Specification and verification of component-based systems","first-page":"11","article-title":"Typestate protocol specification in JML","author":"Kim","year":"2009"},{"issue":"5","key":"10.1016\/j.jss.2019.110450_bib0113","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1745312.1745313","article-title":"A hybrid type system for lock-freedom of mobile processes","volume":"32","author":"Kobayashi","year":"2010","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/j.jss.2019.110450_bib0114","series-title":"Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering - ICSE \u201910","article-title":"Detecting atomic-set serializability violations in multithreaded programs through active randomized testing","author":"Lai","year":"2010"},{"key":"10.1016\/j.jss.2019.110450_bib0115","series-title":"Formal Methods and Software Engineering: 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12\u201316, 2012. Proceedings","first-page":"5","article-title":"Variable permissions for concurrency verification","author":"Le","year":"2012"},{"issue":"3","key":"10.1016\/j.jss.2019.110450_bib0116","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1127878.1127884","article-title":"Preliminary design of JML: a behavioral interface specification language for Java","volume":"31","author":"Leavens","year":"2006","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"10.1016\/j.jss.2019.110450_bib0118","series-title":"European Symposium on Programming","first-page":"378","article-title":"A basis for verifying multi-threaded programs","author":"Leino","year":"2009"},{"key":"10.1016\/j.jss.2019.110450_bib0119","series-title":"Foundations of Security Analysis and Design V: FOSAD 2007\/2008\/2009 Tutorial Lectures","first-page":"195","article-title":"Verification of Concurrent Programs with Chalice","author":"Leino","year":"2009"},{"issue":"2","key":"10.1016\/j.jss.2019.110450_bib0120","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1145\/1353535.1346323","article-title":"Learning from mistakes","volume":"42","author":"Lu","year":"2008","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"10.1016\/j.jss.2019.110450_bib0121","series-title":"2013 35th International Conference on Software Engineering (ICSE)","first-page":"322","article-title":"Detecting deadlock in programs with data-centric synchronization","author":"Marino","year":"2013"},{"key":"10.1016\/j.jss.2019.110450_bib0122","series-title":"Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology - HILT \u201914","first-page":"103","article-title":"The rust language","author":"Matsakis","year":"2014"},{"key":"10.1016\/j.jss.2019.110450_bib0123","series-title":"Object-Oriented Software Construction","author":"Meyer","year":"1988"},{"issue":"10","key":"10.1016\/j.jss.2019.110450_bib0124","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","article-title":"Applying \u2019design by contract\u2019","volume":"25","author":"Meyer","year":"1992","journal-title":"Computer"},{"key":"10.1016\/j.jss.2019.110450_bib0125","series-title":"Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs","first-page":"7:1","article-title":"Aliasing Control with View-based Typestate","author":"Militao","year":"2010"},{"key":"10.1016\/j.jss.2019.110450_bib0126","series-title":"ECOOP 2014 \u2013 Object-Oriented Programming","first-page":"334","article-title":"Rely-Guarantee Protocols","author":"Milit\u00e3o","year":"2014"},{"key":"10.1016\/j.jss.2019.110450_bib0127","series-title":"Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages Meets Program Verification","first-page":"15","article-title":"Substructural Typestates","author":"Milit\u00e3o","year":"2014"},{"key":"10.1016\/j.jss.2019.110450_bib0128","series-title":"30th European Conference on Object-Oriented Programming, ECOOP 2016","first-page":"161","article-title":"Composing interfering abstract: Protocols","volume":"56","author":"Milit\u00e3o","year":"2016"},{"key":"10.1016\/j.jss.2019.110450_bib0129","series-title":"INFORUM 2009 - Simpsio de Informtica","first-page":"1","article-title":"An Exception Aware Behavioral Type System for Object-Oriented Programs","author":"Milit\u00e3o","year":"2009"},{"key":"10.1016\/j.jss.2019.110450_bib0130","series-title":"Typed Lambda Calculi and Applications","first-page":"293","article-title":"L3: A Linear Language with Locations","author":"Morrisett","year":"2005"},{"key":"10.1016\/j.jss.2019.110450_bib0131","series-title":"Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications - OOPSLA \u201907","article-title":"Ownership transfer in universe types","author":"M\u00fcller","year":"2007"},{"key":"10.1016\/j.jss.2019.110450_bib0132","series-title":"Verification, Model Checking, and Abstract Interpretation","first-page":"41","article-title":"Viper: A verification infrastructure for permission-based reasoning","author":"M\u00fcller","year":"2016"},{"key":"10.1016\/j.jss.2019.110450_bib0133","series-title":"Dependable Software Systems Engineering","article-title":"Viper: A Verification Infrastructure for Permission-based Reasoning","author":"M\u00fcller","year":"2017"},{"key":"10.1016\/j.jss.2019.110450_bib0134","series-title":"Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"557","article-title":"A Type System for Borrowing Permissions","author":"Naden","year":"2012"},{"key":"10.1016\/j.jss.2019.110450_bib0135","series-title":"Proceedings - International Conference on Software Engineering","article-title":"Effective static deadlock detection","author":"Naik","year":"2009"},{"key":"10.1016\/j.jss.2019.110450_bib0136","series-title":"Proceedings of the 20th International Conference on Computer Aided Verification","first-page":"355","article-title":"Enhancing program verification with lemmas","author":"Nguyen","year":"2008"},{"key":"10.1016\/j.jss.2019.110450_bib0137","series-title":"From CML to Process Algebras","first-page":"493","author":"Nielson","year":"1993"},{"key":"10.1016\/j.jss.2019.110450_bib0138","doi-asserted-by":"crossref","DOI":"10.1016\/0304-3975(95)00017-8","article-title":"From CML to its Process Algebra","author":"Nielson","year":"1996","journal-title":"Theor. Comput. Sci"},{"key":"10.1016\/j.jss.2019.110450_bib0139","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","article-title":"Flexible alias protection","author":"Noble","year":"1998"},{"key":"10.1016\/j.jss.2019.110450_bib0140","series-title":"Technical Report","article-title":"An overview of the Scala programming language","author":"Odersky","year":"2004"},{"key":"10.1016\/j.jss.2019.110450_bib0141","series-title":"Computer Science Logic","first-page":"1","article-title":"Local Reasoning about Programs that Alter Data Structures","author":"O\u2019Hearn","year":"2001"},{"issue":"1-3","key":"10.1016\/j.jss.2019.110450_bib0142","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","article-title":"Resources, concurrency, and local reasoning","volume":"375","author":"OHearn","year":"2007","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"10.1016\/j.jss.2019.110450_bib0143","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1145\/360051.360224","article-title":"Verifying properties of parallel programs: An axiomatic approach","volume":"19","author":"Owicki","year":"1976","journal-title":"Commun. ACM"},{"key":"10.1016\/j.jss.2019.110450_bib0144","article-title":"PVS: a prototype verification system","author":"Owre","year":"1992","journal-title":"11th International Conference on Automated Deduction"},{"issue":"1","key":"10.1016\/j.jss.2019.110450_bib0145","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1145\/1047659.1040326","article-title":"Separation logic and abstraction","volume":"40","author":"Parkinson","year":"2005","journal-title":"ACM SIGPLAN Notices"},{"key":"10.1016\/j.jss.2019.110450_bib0146","series-title":"Proceedings of the 31st Annual ACM Symposium on Applied Computing","first-page":"1806","article-title":"From Atomic Variables to Data-centric Concurrency Control","author":"Paulino","year":"2016"},{"key":"10.1016\/j.jss.2019.110450_bib0147","series-title":"Proceedings - International Conference on Software Engineering","article-title":"Statically checking API protocol conformance with mined multi-object specifications","author":"Pradel","year":"2012"},{"key":"10.1016\/j.jss.2019.110450_bib0148","series-title":"Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages","first-page":"39","article-title":"Syntactic Control of Interference","author":"Reynolds","year":"1978"},{"key":"10.1016\/j.jss.2019.110450_bib0149","series-title":"Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on","first-page":"55","article-title":"Separation logic: A logic for shared mutable data structures","author":"Reynolds","year":"2002"},{"key":"10.1016\/j.jss.2019.110450_bib0150","series-title":"ECOOP 2005 - Object-Oriented Programming","article-title":"Extending JML for Modular Specification and Verification of Multi-threaded Programs","author":"Rodr\u00edguez","year":"2005"},{"key":"10.1016\/j.jss.2019.110450_bib0151","series-title":"Second {NASA} Formal Methods Symposium - {NFM} 2010, Washington D.C., USA, April 13-15, 2010. Proceedings","first-page":"222","article-title":"Model Checking with Edge-valued Decision Diagrams","author":"Roux","year":"2010"},{"key":"10.1016\/j.jss.2019.110450_sbref0150","author":"Sadiq","year":"2019","journal-title":"Automatic inference of symbolic permissions for sequential java programs"},{"key":"10.1016\/j.jss.2019.110450_bib0153","series-title":"21st International Conference on Engineering of Complex Computer Systems, United Arab Emirates, November 6-8, 2016","first-page":"215","article-title":"Extracting Permission-Based Specifications from a Sequential Java Program","author":"Sadiq","year":"2016"},{"key":"10.1016\/j.jss.2019.110450_bib0154","series-title":"Proceedings of the 34rd ACM\/IEEE International Conference on Automated Software Engineering, ASE 2019, 2019","article-title":"Sip4j: Statically inferring access permission contracts for parallelising sequential java programs","author":"Sadiq","year":"2019"},{"key":"10.1016\/j.jss.2019.110450_bib0155","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1016\/S0304-3975(99)00040-7","article-title":"The name discipline of uniform receptiveness","volume":"221","author":"Sangiorgi","year":"1999","journal-title":"Theor. Comput. Sci"},{"issue":"3","key":"10.1016\/j.jss.2019.110450_bib0156","doi-asserted-by":"crossref","DOI":"10.2168\/LMCS-7(3:21)2011","article-title":"Nested hoare triples and frame rules for higher-order store","volume":"7","author":"Schwinghammer","year":"2011","journal-title":"Logical Methods in Computer Science"},{"key":"10.1016\/j.jss.2019.110450_bib0157","series-title":"ECOOP 2007 \u2013 Object-Oriented Programming","first-page":"2","article-title":"Gradual typing for objects","author":"Siek","year":"2007"},{"key":"10.1016\/j.jss.2019.110450_bib0158","article-title":"Automated verification of specifications with typestates and access Permissions","volume":"53","author":"Siminiceanu","year":"2012","journal-title":"ECEASST"},{"key":"10.1016\/j.jss.2019.110450_bib0159","series-title":"Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic","first-page":"148","author":"Smans","year":"2009"},{"issue":"1","key":"10.1016\/j.jss.2019.110450_bib0160","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2543920","article-title":"aem: A permission-based concurrent-by-default programming language approach","volume":"36","author":"Stork","year":"2014","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"10.1016\/j.jss.2019.110450_bib0161","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","article-title":"Typestate: A programming language concept for enhancing software reliability","author":"Strom","year":"1986","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/j.jss.2019.110450_bib0162","doi-asserted-by":"crossref","DOI":"10.1145\/2076021.2048122","article-title":"First-class state change in plaid","author":"Sunshine","year":"2011","journal-title":"ACM SIGPLAN Notices"},{"key":"10.1016\/j.jss.2019.110450_bib0163","series-title":"In PARLE94, volume 817 of LNCS","first-page":"398","article-title":"An interaction-based language and its typing system","author":"Takeuchi","year":"1994"},{"key":"10.1016\/j.jss.2019.110450_bib0164","series-title":"CONCUR 2007 \u2013 Concurrency Theory","first-page":"256","article-title":"A Marriage of Rely\/Guarantee and Separation Logic","author":"Vafeiadis","year":"2007"},{"key":"10.1016\/j.jss.2019.110450_bib0165","series-title":"Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"334","article-title":"Associating Synchronization Constraints with Data in an Object-oriented Language","author":"Vaziri","year":"2006"},{"key":"10.1016\/j.jss.2019.110450_bib0166","series-title":"ECOOP 2010 \u2013 Object-Oriented Programming","first-page":"304","article-title":"A Type System for Data-Centric Synchronization","author":"Vaziri","year":"2010"},{"key":"10.1016\/j.jss.2019.110450_bib0167","series-title":"Programming Languages and Systems","first-page":"194","article-title":"Proving copyless message passing","author":"Villard","year":"2009"},{"key":"10.1016\/j.jss.2019.110450_bib0168","series-title":"Tracking Heaps That Hop with Heap-Hop","first-page":"275","author":"Villard","year":"2010"},{"issue":"2","key":"10.1016\/j.jss.2019.110450_bib0169","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1022920129859","article-title":"Model checking programs","volume":"10","author":"Visser","year":"2003","journal-title":"Automated Software Engineering"},{"key":"10.1016\/j.jss.2019.110450_bib0170","series-title":"Proceedings of 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering - ESEC-FSE \u201907","first-page":"205","article-title":"RELAY","author":"Voung","year":"2007"},{"key":"10.1016\/j.jss.2019.110450_bib0171","series-title":"J. Funct. Program","article-title":"Propositions as sessions","author":"Wadler","year":"2014"},{"key":"10.1016\/j.jss.2019.110450_bib0172","series-title":"Proceedings of the 26th European Conference on Object-Oriented Programming","first-page":"614","article-title":"Practical Permissions for Race-free Parallelism","author":"Westbrook","year":"2012"},{"issue":"6","key":"10.1016\/j.jss.2019.110450_bib0173","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1064978.1065013","article-title":"A serializability violation detector for shared-memory server programs","volume":"40","author":"Xu","year":"2005","journal-title":"ACM SIGPLAN Notices"},{"key":"10.1016\/j.jss.2019.110450_bib0174","series-title":"Concurrency analysis based on fractional permissions","author":"Zhao","year":"2007"},{"key":"10.1016\/j.jss.2019.110450_bib0175","series-title":"2008 International Conference on Advanced Computer Theory and Engineering","first-page":"709","article-title":"The Permission Approach to Comprehend Lock-Based Synchronization Policy","author":"Zhao","year":"2008"}],"container-title":["Journal of Systems and Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0164121219302249?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0164121219302249?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,21]],"date-time":"2020-01-21T04:23:29Z","timestamp":1579580609000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0164121219302249"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1]]},"references-count":173,"alternative-id":["S0164121219302249"],"URL":"https:\/\/doi.org\/10.1016\/j.jss.2019.110450","relation":{},"ISSN":["0164-1212"],"issn-type":[{"value":"0164-1212","type":"print"}],"subject":[],"published":{"date-parts":[[2020,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"A survey on the use of access permission-based specifications for program verification","name":"articletitle","label":"Article Title"},{"value":"Journal of Systems and Software","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jss.2019.110450","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2019 Elsevier Inc. All rights reserved.","name":"copyright","label":"Copyright"}],"article-number":"110450"}}