caa a22 4500 605516170 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20150501xx s 000 0 eng 10.1007/s00165-014-0310-2 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0310-2 Balancing expressiveness in formal approaches to concurrency [Elektronische Daten] [Cliff Jones, Ian Hayes, Robert Colvin] One might think that specifying and reasoning about concurrent programs would be easier with more expressive languages. This paper questions that view. Clearly too weak a notation can mean that useful properties either cannot be expressed or their expression is unnatural. But choosing too powerful a notation also has its drawbacks since reasoning receives little guidance. For example, few would suggest that programming languages themselves provide tractable specifications. Both rely/guarantee methods and separation logic(s) provide useful frameworks in which it is natural to reason about aspects of concurrency. Rather than pursue an approach of extending the notations of either approach, this paper starts with the issues that appear to be inescapable with concurrency and—only as a response thereto—examines ways in which these fundamental challenges can be met. Abstraction is always a ubiquitous tool and its influence on how the key issues are tackled is examined in each case. The Author(s), 2014 Concurrency nationallicence Rely/guarantee reasoning nationallicence Separation logic nationallicence Jones Cliff School of Computing Science, Newcastle University, Newcastle Upon Tyne NE1 7RU, UK aut Hayes Ian School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Brisbane, Australia aut Colvin Robert School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Brisbane, Australia aut Formal Aspects of Computing Springer London 27/3(2015-05-01), 475-497 0934-5043 27:3<475 2015 27 165 https://doi.org/10.1007/s00165-014-0310-2 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0310-2 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Jones Cliff School of Computing Science, Newcastle University, Newcastle Upon Tyne NE1 7RU, UK aut NATIONALLICENCE 700 1- Hayes Ian School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Brisbane, Australia aut NATIONALLICENCE 700 1- Colvin Robert School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Brisbane, Australia aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/3(2015-05-01), 475-497 0934-5043 27:3<475 2015 27 165