@comment{{This file has been generated by bib2bib 1.98}}

@comment{{Command line: bib2bib -c '$key="FM2016atomicSteps" or $key="AFfGRGRACP" or $key="jon83a" or $key="Jones81d" or $key="DaSMfaWSLwC" or $key="fixedpointcalculus1995" or 1=2' ./root.bib}}

@article{jon83a,
  author = {C.B. Jones},
  title = {Tentative steps toward a development method for interfering programs},
  keywords = {rely guarantee},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = 5,
  number = 4,
  pages = {596-619},
  month = oct,
  year = 1983
}

@phdthesis{Jones81d,
  author = {C. B. Jones},
  date-modified = {2014-03-07 15:12:08 +0000},
  local-url = {./Other-TRs/Jon81_thesis_PRG_25.pdf},
  month = {June},
  note = {Available as: Oxford University Computing Laboratory (now Computer Science) Technical Monograph PRG-25},
  onote = {Printed as: Programming Research Group, Technical Monograph 25},
  school = {Oxford University},
  title = {Development Methods for Computer Programs including a Notion of Interference},
  year = {1981}
}

@article{fixedpointcalculus1995,
  author = {Chritiene Aarts and Roland Backhouse and Eerke Boiten and Henk Doombos and Netty van Gasteren and Rik van Geldrop and Paul Hoogendijk and Ed Voermans and Jaap van der Woude},
  note = {{Mathematics of Program Construction Group.}},
  title = {Fixed-point calculus},
  journal = {Information Processing Letters},
  volume = {53},
  pages = {131--136},
  year = {1995}
}

@article{AFfGRGRACP,
  author = {I. J. Hayes},
  oauthor = {Ian J. Hayes},
  title = {Generalised rely-guarantee concurrency: An algebraic foundation},
  journal = {Formal Aspects of Computing},
  volume = {28},
  number = {6},
  pages = {1057--1078},
  issn = {0934-5043},
  doi = {10.1007/s00165-016-0384-0},
  url = {https://doi.org/10.1007/s00165-016-0384-0},
  submitted = {Submitted 22 April 2014},
  accepted = {Accepted 17 June 2016},
  online = {Online 29 July 2016},
  publisher = {Springer London},
  keywords = {Concurrent programming; rely-guarantee concurrency;
    program verification; program algebra.},
  acm = {D.1.3; D.2.4},
  language = {English},
  abstract = {
    The rely-guarantee technique allows one to reason compositionally about
    concurrent programs. To handle interference the technique makes use of rely and
    guarantee conditions, both of which are binary relations on states. A rely
    condition is an assumption that the environment performs only atomic steps
    satisfying the rely relation and a guarantee is a commitment that every atomic
    step the program makes satisfies the guarantee relation. In order to
    investigate rely-guarantee reasoning more generally, in this paper we allow
    interference to be represented by a process rather than a relation and hence
    derive more general rely-guarantee laws. The paper makes use of a weak
    conjunction operator between processes, which generalises a guarantee relation
    to a guarantee process, and introduces a rely quotient operator, which
    generalises a rely relation to a process. The paper focuses on the algebraic
    properties of the general rely-guarantee theory. The Jones-style rely-guarantee
    theory can be interpreted as a model of the general algebraic theory and hence
    the general laws presented here hold for that theory.
  },
  month = {November},
  year = {2016}
}

@inproceedings{FM2016atomicSteps,
  author = {Ian J. Hayes and Robert J. Colvin and Larissa A. Meinicke and Kirsten Winter and Andrius Velykis},
  oauthor = {I.J. Hayes and R.J. Colvin and L.A. Meinicke and K. Winter and A. Velykis},
  title = {An algebra of synchronous atomic steps},
  booktitle = {FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings},
  editor = {John Fitzgerald and Constance Heitmeyer and Stefania Gnesi and Anna Philippou},
  pages = {352--369},
  accepted = {Accepted 9 August 2016},
  series = {Lecture Notes in Computer Science},
  volume = {9995},
  publisher = {Springer International Publishing},
  address = {Cham},
  optkey = {},
  month = {November},
  isbn = {978-3-319-48989-6},
  doi = {10.1007/978-3-319-48989-6_22},
  url = {https://doi.org/10.1007/978-3-319-48989-6_22},
  year = {2016},
  optannote = {}
}

@article{DaSMfaWSLwC,
  author = {Robert J. Colvin and Ian J. Hayes and Larissa A. Meinicke},
  title = {Designing a semantic model for a wide-spectrum language with concurrency},
  journal = {Formal Aspects of Computing},
  ovolume = {},
  onumber = {??},
  pages = {1--22},
  issn = {0934-5043},
  odoi = {10.1007/s00165-012-??-1},
  ourl = {https://doi.org/10.1007/s00165-012-??-1},
  submitted = {Submitted 22 March 2016, 29 September 2016},
  accepted = {Accepted 28 November 2016},
  note = {Accepted 28 November 2016},
  online = {Online ??},
  publisher = {Springer London},
  keywords = {Refinement calculus; wide-spectrum language; concurrency; program algebra; rely-guarantee},
  acm = {D.1.3; D.2.4},
  language = {English},
  abstract = {
    A wide-spectrum language integrates specification constructs into a
    programming language in a manner that treats a specification command
    just like any other command.  The primary contribution of this paper
    is a semantic model for a wide-spectrum language that supports
    concurrency and a refinement calculus.  A distinguishing feature of
    the language is that steps of the environment are modelled explicitly,
    alongside steps of the program.  From these two types of steps a rich
    set of specification commands can be constructed, based on operators
    for nondeterministic choice, and sequential and parallel composition.  We
    also introduce a novel operator, \emph{weak conjunction}, which is
    used extensively to conjoin separate aspects of specifications,
    allowing us to take a separation-of-concerns approach to subsequent
    reasoning.  We provide a denotational semantics for the language based
    on traces, which may be terminating, aborting, infeasible, or
    infinite.

    To demonstrate the generality and unifying strength of the language,
    we use it to express a range of concepts from the concurrency
    literature, including: a refinement theory for rely/guarantee
    reasoning; an abstract specification of local variables in a
    concurrent context; specification of an abstract, linearisable data
    structure; a partial encoding of temporal logic; and defining the
    relationships between notions of nonblocking programs.  The novelty of
    the paper is that these diverse concepts build on the same theory.  In
    particular, the \emph{rely} concept from Jones' rely/guarantee
    framework, and a stronger \emph{demand} concept that restricts the
    environment, are reused across the different domains to express
    assumptions about the environment.  The language and model form an
    instance of an abstract concurrent program algebra, and this
    facilitates reasoning about properties of the model at a high level of
    abstraction.
  },
  omonth = {??},
  year = {2016}
}

