ARTICLE.bib

@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib -ob ARTICLE.bib -oc ARTICLE-cites -c 'not $key : "TRX$"' -c '$type : "^ARTICLE$"' ../pubs-html.bib}}
@article{CARCGMIA,
  author = {Dongol, B. and Hayes, I. J. and Struth, G.},
  title = {Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras},
  journal = {Logical Methods in Computer Science},
  issue_date = {??},
  volume = {17},
  number = {1},
  month = feb,
  issn = {1860-5974},
  pages = {13:1--13:34},
  articleno = {13},
  numpages = {34},
  doi = {10.23638/LMCS-17(1:13)2021},
  keywords = {relational convolution, relational semigroup, partial semigroup, quantale, convolution algebra, modal algebra, substructural logics, interval logics, duration calculus},
  datepublished = {2017-02-09},
  submitted = {Submitted 6 July 2017},
  accepted = {Accepted 13 Jan 2021},
  for = {080203 (Computational Logic and Formal Languages)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP190102142 DV4CS},
  abstract = {
    Convolution is a ubiquitous operation in mathematics and computing.
    The Kripke semantics for substructural and interval logics motivates
    its study for quantale-valued functions relative to ternary relations.
    The resulting notion of relational convolution leads to generalised
    binary and unary modal operators for qualitative and quantitative models,
    and to more conventional variants, when ternary relations arise from
    identities over partial semigroups. Convolution-based semantics for
    fragments of categorial, linear and incidence (segment or interval) logics
    are provided as qualitative applications. Quantitative examples include
    algebras of durations and mean values in the duration calculus. 
  },
  year = {2021}
}
@article{DSoCPfCPS_2019,
  author = {Burns, A. and Hayes, I. J. and Jones, C. B.},
  title = {Deriving Specifications of Control Programs for Cyber Physical Systems},
  journal = {The Computer Journal},
  volume = {63},
  number = {5},
  pages = {774--790},
  month = {May},
  publisher = {BCS/Oxford Academic},
  online = {First published online: 30 April 2019},
  accepted = {Accepted 25 February 2019},
  submission = {Journal submission 8th August 2018; revised 6 December 2018},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP190102142 DV4CS},
  keywords = {Cyber-physical systems; real-time systems; time bands; rely-guarantee; concurrency; embedded systems},
  abstract = {
    Cyber physical systems (CPS) exist in a physical environment and comprise both physical
    components and a control program. Physical components are inherently liable to failure and yet
    an overall CPS is required to operate safely, reliably and cost effectively. This paper proposes
    a framework for deriving the specification of the software control component of a CPS from an
    understanding of the behaviour required of the overall system in its physical environment. The
    two key elements of this framework are (i) an extension to the use of rely/guarantee conditions to
    allow specifications to be obtained systematically from requirements (as expressed in terms of the
    required behaviour in the environment) and nested assumptions (about the physical components of
    the CPS); and (ii) the use of time bands to record the temporal properties required of the CPS at
    a number of different granularities. The key contribution is in combining these ideas; using time
    bands overcomes a significant drawback in earlier work. The paper also addresses the means by
    which the reliability of a CPS can be addressed by challenging each rely condition in the derived
    specification and, where appropriate, improve robustness and/or define weaker guarantees that can
    be delivered with respect to the corresponding weaker rely conditions.
  },
  issn = {0010-4620},
  doi = {10.1093/comjnl/bxz019},
  url = {https://doi.org/10.1093/comjnl/bxz019},
  oeprint = {https://academic.oup.com/comjnl/article-pdf/63/5/774/33222417/bxz019.pdf},
  year = {2020}
}
@article{FMJournalAtomicSteps,
  author = {Ian J. Hayes and Larissa A. Meinicke and Kirsten Winter and Robert J. Colvin},
  title = {A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency},
  journal = {Formal Aspects of Computing},
  volume = {31},
  number = {2},
  pages = {133--163},
  issn = {0934-5043},
  doi = {10.1007/s00165-018-0464-4},
  submitted = {Submitted 26 September 2017},
  accepted = {Accepted 11 June 2018},
  online = {Online 6 August 2018},
  publisher = {Springer London},
  keywords = {Refinement calculus; synchronous parallel; concurrency; program algebra; rely-guarantee},
  acm = {D.1.3; D.2.4},
  language = {English},
  abstract = {
    In this paper we introduce an abstract algebra for reasoning about
    concurrent programs, that includes an abstract algebra of atomic
    steps, with sub-algebras of program and environment steps, and an
    abstract synchronisation operator.
    We show how the abstract synchronisation operator can be
    instantiated as a synchronous parallel operator with
    interpretations in rely-guarantee concurrency for shared-memory
    systems, and in process algebras CCS and CSP. 
    It is also instantiated as a weak conjunction operator, an operator
    that is useful for the specification of rely and guarantee conditions
    in rely/guarantee concurrency.
    The main differences between the parallel and weak conjunction
    instantiations of the synchronisation operator are how they combine
    individual atomic steps.
    Lemmas common to these different instantiations are proved once using
    the axiomatisation of the abstract synchronous operator.
    
    Using the sub-algebras of program and environment atomic steps, rely
    and guarantee conditions, as well as Morgan-style specification 
    commands, are defined at a high-level of abstraction in the program
    algebra. Lifting these concepts from rely/guarantee concurrency to a
    higher level of abstraction makes them more widely applicable.
    We demonstrate the practicality of the algebra by showing how a core
    law from rely-guarantee theory, the parallel introduction law, can be
    abstracted and verified easily in the algebra. 
    In addition to proving fundamental properties for reasoning about
    concurrent shared-variable programs, the algebra is instantiated 
    to prove abstract process synchronisation properties familiar from
    the process algebras CCS and CSP.  
    
    The algebra has been encoded in Isabelle/HOL to provide a basis for
    tool support for concurrent program verification based on the
    rely/guarantee technique. It facilitates simpler, more general, proofs
    that allow a higher level of automation than what is possible in
    low-level, model-specific interpretations.
  },
  project = {DP190102142 DV4CS, DP130102901 RGT as ArXiV only},
  month = {April},
  year = {2019}
}
@article{PSemigroupsConvolution-AFP,
  author = {Brijesh Dongol and Victor B. F. Gomes and Ian J. Hayes and Georg Struth},
  title = {Partial Semigroups and Convolution Algebras},
  journal = {Archive of Formal Proofs},
  note = {\url{https://www.isa-afp.org/entries/PSemigroupsConvolution.shtml},
            Formal proof development},
  issn = {2150-914x},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  abstract = {Partial Semigroups are relevant to the foundations of quantum mechanics and combinatorics
    as well as to interval and separation logics. Convolution algebras can be understood either as
    algebras of generalised binary modalities over ternary Kripke frames, in particular over partial
    semigroups, or as algebras of quantale-valued functions which are equipped with a
    convolution-style operation of multiplication that is parametrised by a ternary relation.
    Convolution algebras provide algebraic semantics for various substructural logics, including
    categorial, relevance and linear logics, for separation logic and for interval logics; they cover
    quantitative and qualitative applications. These mathematical components for partial
    semigroups and convolution algebras provide uniform foundations from which models of
    computation based on relations, program traces or pomsets, and verification components for
    separation or interval temporal logics can be built with little effort. 
  },
  month = jun,
  year = 2017
}
@article{DaSMfaWSLwC,
  author = {R. J. Colvin and I. J. Hayes and L. A. Meinicke},
  title = {Designing a semantic model for a wide-spectrum language with concurrency},
  journal = {Formal Aspects of Computing},
  volume = {29},
  pages = {853-875},
  issn = {0934-5043},
  submitted = {Submitted 22 March 2016, 29 September 2016},
  accepted = {Accepted 28 November 2016},
  online = {Online 27 February 2017},
  note = {Online 27 February 2017},
  publisher = {Springer London},
  keywords = {Refinement calculus; wide-spectrum language; concurrency; program algebra; rely-guarantee},
  acm = {D.1.3; D.2.4},
  language = {English},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  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.
  },
  year = {2017}
}
@article{Concurrent_Ref_Alg-AFP,
  author = {J. Fell and I. J. Hayes and A. Velykis},
  title = {Concurrent Refinement Algebra and Rely Quotients},
  journal = {Archive of Formal Proofs},
  note = {\url{http://isa-afp.org/entries/Concurrent_Ref_Alg.shtml},
            Formal proof development},
  issn = {2150-914x},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  abstract = {
    The concurrent refinement algebra developed here is designed to provide
    a foundation for rely/guarantee reasoning about concurrent programs.
    The algebra builds on a complete lattice of commands by providing
    sequential composition, parallel composition and a novel weak conjunction operator.
    The weak conjunction operator coincides with the lattice supremum
    providing its arguments are non-aborting, but aborts if either of its arguments do.
    Weak conjunction provides an abstract version of a guarantee condition as a guarantee process.
    We distinguish between models that distribute sequential composition
    over non-deterministic choice from the left (referred to as being conjunctive
    in the refinement calculus literature) and those that don't.
    Least and greatest fixed points of monotone functions are provided to
    allow recursion and iteration operators to be added to the language.
    Additional iteration laws are available for conjunctive models.
    The rely quotient of processes c and i is the process that,
    if executed in parallel with i implements c.
    It represents an abstract version of a rely condition generalised to a process.
  },
  month = dec,
  year = 2016
}
@article{AFfGRGRACP,
  author = {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 = {http://dx.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},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  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}
}
@article{PVEaCfC,
  author = {Cliff B. Jones and Ian J. Hayes},
  title = {Possible values: Exploring a concept for concurrency},
  journal = {Journal of Logical and Algebraic Methods in Programming},
  volume = {85},
  number = {5, Part 2},
  pages = {972--984},
  month = {August},
  accepted = {Accepted 8 January 2016. Available online 13 January 2016},
  issn = {2352-2208},
  doi = {http://dx.doi.org/10.1016/j.jlamp.2016.01.002},
  url = {http://www.sciencedirect.com/science/article/pii/S2352220816000031},
  keywords = {Concurrent programming},
  keywords = {Rely/guarantee conditions},
  keywords = {Possible values},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  abstract = {An important issue in concurrency is interference. This issue manifests itself in both shared-variable and communication-based concurrency -- this paper focusses on the former case where interference is caused by the environment of a process changing the values of shared variables. Rely/guarantee approaches have been shown to be useful in specifying and reasoning compositionally about concurrent programs. This paper explores the use of a ``possible values'' notation for reasoning about variables whose values can be changed multiple times by interference. Apart from the value of this concept in providing clear specifications, it offers a principled way of avoiding the need for some auxiliary (or ghost) variables whose unwise use can destroy compositionality.},
  year = {2016}
}
@article{CaaUC,
  author = {Dongol, B. and Hayes, I. J. and Struth, G.},
  title = {Convolution As a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency},
  journal = {ACM Trans. Comput. Logic},
  issue_date = {February 2016},
  volume = {17},
  number = {3},
  month = feb,
  issn = {1529-3785},
  pages = {15:1--15:25},
  articleno = {15},
  numpages = {25},
  url = {http://doi.acm.org/10.1145/2874773},
  doi = {10.1145/2874773},
  acmid = {2874773},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {Concurrency, Hoare logics, convolution, formal power series, formal semantics, interval logics, quantales, semigroups, separation logics, systems verification},
  datepublished = {2016-02-17},
  submitted = {Submitted 6 November 2014, Revised 23 May 2015},
  accepted = {Accepted 14 November 2015},
  for = {080203 (Computational Logic and Formal Languages)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  abstract = {
    A notion of convolution is presented in the context of formal power series
    together with lifting constructions characterising algebras of such series,
    which usually are quantales.
    A number of examples underpin the universality of these constructions,
    the most prominent ones being separation logics,
    where convolution is separating conjunction in an assertion quantale;
    interval logics, where convolution is the chop operation;
    and stream interval functions,
    where convolution is proposed for analysing the trajectories of dynamical or real-time systems.
    A Hoare logic can be constructed in a generic fashion on the power-series quantale,
    which applies to each of these examples.
    In many cases, commutative notions of convolution have natural interpretations as concurrency operations.
  },
  year = {2016}
}
@article{FACJexSEFM-14,
  author = {Cliff B. Jones and Ian J. Hayes and Robert J. Colvin},
  title = {Balancing Expressiveness in Formal Approaches to Concurrency},
  journal = {Formal Aspects of Computing},
  issn = {0934-5043},
  volume = {27},
  number = {3},
  pages = {475--497},
  accepted = {Accepted 8 July 2014},
  online = {29 August 2014},
  publisher = {Springer London},
  doi = {10.1007/s00165-014-0310-2},
  url = {http://dx.doi.org/10.1007/s00165-014-0310-2},
  keywords = {Concurrency; Rely/guarantee reasoning; Separation logic},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  abstract = {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.},
  month = {May},
  year = {2015}
}
@article{DHR14,
  author = {Brijesh Dongol and Ian J. Hayes and Peter J. Robinson},
  title = {Reasoning about Goal-Directed Real-Time Teleo-Reactive Programs},
  journal = {Formal Aspects of Computing},
  volume = {26},
  number = {3},
  pages = {563-589},
  issn = {0934-5043},
  doi = {10.1007/s00165-012-0272-1},
  url = {http://dx.doi.org/10.1007/s00165-012-0272-1},
  accepted = {Accepted 20-11-2012},
  online = {8 Jan 2013},
  publisher = {Springer London},
  keywords = {Teleo-reactive programming; Goal-directed agents; 
    Rely/guarantee reasoning; Real-time programs; Reactive systems; Interval-based logics},
  language = {English},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT/DP0987452 TFTR},
  abstract = {
    The teleo-reactive programming model is a high-level approach to 
    developing real-time systems that supports hierarchical composition 
    and durative actions. The model is different from frameworks such as 
    action systems, timed automata and TLA+, and allows programs to 
    be more compact and descriptive of their intended 
    behaviour. Teleo-reactive programs are particularly useful for 
    implementing controllers for autonomous agents that must react 
    robustly to their dynamically changing environments. In this paper, 
    we develop a real-time logic that is based on Duration Calculus 
    and use this logic to formalise the semantics of teleo-reactive 
    programs. We develop rely/guarantee rules that facilitate reasoning 
    about a program and its environment in a compositional manner. We 
    present several theorems for simplifying proofs of teleo-reactive 
    programs and present a partially mechanised method for proving 
    progress properties of goal-directed agents.
  },
  month = {May},
  year = {2014}
}
@article{DRTASwMTBUAR,
  author = {Brijesh Dongol and Ian J. Hayes and John Derrick},
  title = {Deriving real-time action systems with multiple time bands using algebraic reasoning},
  journal = {Science of Computer Programming},
  pages = {137--165},
  volume = {85 Part B},
  issn = {0167-6423},
  doi = {10.1016/j.scico.2013.08.009},
  publisher = {Elsevier},
  accepted = {14 August 2013},
  oonline = {?? Aug 2012},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  abstract = {
    The verify-while-develop paradigm allows one to incrementally develop programs from their specifications 
    using a series of calculations against the remaining proof obligations. This paper presents a derivation 
    method for real-time systems with realistic constraints on their behaviour. We develop a high-level
    interval-based logic that provides flexibility in an implementation, yet allows algebraic reasoning over multiple 
    granularities and sampling multiple sensors with delay. The semantics of an action system is given in terms 
    of interval predicates and algebraic operators to unify the logics for an action system and its properties, 
    which in turn simplifies the calculations and derivations.
  },
  keywords = {Action systems},
  keywords = {Enforced properties},
  keywords = {Program refinement},
  keywords = {Derivation},
  keywords = {True concurrency},
  year = 2014
}
@article{CDoNiEE,
  author = {I. J. Hayes and A. Burns and B. Dongol and C. B. Jones},
  title = {Comparing Degrees of Non-Deterministic in Expression Evaluation},
  journal = {The Computer Journal},
  pages = {741--755},
  volume = {56},
  number = {6},
  publisher = {BCS},
  online = {First published online: February 5, 2013},
  accepted = {Accepted 4 January 2013},
  submission = {Journal submission 25 January 2012; revised 21 November 2012},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  keywords = {non-deterministic expression evaluation; sampling logic; rely-guarantee;
              concurrency; real-time programming},
  abstract = {
    Expression evaluation in programming languages is normally assumed to be deterministic;
    however, if an expression involves variables that are being modified by the environment
    of the process during its evaluation, the result of the evaluation can be non-deterministic.
    Two common scenarios in which this occurs are concurrent programs within which processes
    share variables and real-time programs that interact to monitor and/or control their environment.
    In these contexts, although any particular evaluation of an expression gives a single result,
    there is a range of possible values that could be returned depending on the relative timing between
    modification of a variable by the environment and its access within the expression evaluation.
    To compare the semantics of non-deterministic expression evaluation, one can use the set of
    possible values the expression evaluation could return.
    This paper formalizes three approaches to non-deterministic expression evaluation,
    highlights their commonalities and differences, shows the relationships between the approaches
    and explores conditions under which they coincide.
    Modal operators representing that a predicate holds for all possible evaluations and
    for some possible evaluation are associated with each of the evaluation approaches,
    and the properties and relationships between these operators are investigated.
    Furthermore, a link is made to a new notation used in reasoning about interference.
  },
  year = {2013}
}
@article{DRTASiaSL,
  author = {Brijesh Dongol and Ian J. Hayes},
  title = {Deriving real-time action systems in a sampling logic},
  journal = {Science of Computer Programming},
  volume = {78},
  number = {11},
  pages = {2047--2063},
  issn = {0167-6423},
  doi = {10.1016/j.scico.2012.07.008},
  url = {http://www.sciencedirect.com/science/article/pii/S0167642312001360},
  publisher = {Elsevier},
  accepted = {16 October 2011},
  published = {1 November 2013},
  online = {23 Aug 2012},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  era = {ERA 2012 Listed ERA 2010 Rank A},
  project = {DP0987452 TFTR},
  abstract = {
    Action systems have been shown to be applicable for modelling and constructing systems 
    in both discrete and hybrid domains. We present a novel semantics for action systems 
    using a sampling logic that facilitates reasoning about the truly concurrent behaviour 
    between an action system and its environment. By reasoning over the apparent states, the 
    sampling logic allows one to determine whether a state predicate is definitely or possibly 
    true over an interval. We present a semantics for action systems that allows the time taken 
    to sample inputs and evaluate expressions (and hence guards) into account. We develop a 
    temporal logic based on the sampling logic that facilitates formalisation of safety, progress, 
    timing and transient properties. Then, we incorporate this logic to the method of enforced 
    properties, which facilitates stepwise refinement of action systems.
  },
  keywords = {Sampling logic},
  keywords = {Action systems},
  keywords = {Temporal logic},
  keywords = {Enforced properties},
  keywords = {Program refinement},
  keywords = {Derivation},
  keywords = {True concurrency},
  keywords = {Safety-critical systems},
  year = 2013
}
@article{LUToPR,
  author = {I. J. Hayes and S. E. Dunne and L. A. Meinicke},
  title = {Linking Unifying Theories of Program Refinement},
  journal = {Science of Computer Programming},
  pages = {2086--2107},
  volume = {78},
  number = {11},
  publisher = {Elsevier},
  issn = {0167-6423},
  doi = {10.1016/j.scico.2012.07.010},
  url = {http://www.sciencedirect.com/science/article/pii/S0167642312001384},
  online = {Available online 14 August 2012},
  accepted = {Accepted 11 August 2011},
  published = {1 November 2013},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  keywords = {Unifying theories of programming (UTP), Real-time refinement, Program termination},
  abstract = {
    In this paper we consider three theories of programs and specifications at different levels 
    of abstraction. The theories we focus on are: the basic Unifying Theories of Programming 
    (UTP) model, which corresponds to the theories of VDM, B, and the refinement calculus; an 
    extended theory that distinguishes abort from nontermination; and a further extension 
    that introduces (abstract) time. We define UTP-style designs (or specifications) in each 
    theory and show how program constructors, such as nondeterministic choice and 
    sequential composition, can be expressed as single designs in each theory. 
    To examine the relationships between the theories, we construct mappings in both 
    directions between pairs of theories and show that the pairs of mappings form Galois 
    connections. This shows that the simpler (more abstract) models are sub-theories of the 
    more complex extensions. The mappings preserve the program structure and hence are 
    homomorphisms. An important property of a Galois connection is that both mappings 
    preserve refinement. The Galois connections between the models can be exploited to 
    translate properties, including refinement laws, between theories. In addition, we show 
    how to define an iteration in the extended model in terms of an iteration in the timed model.
    },
  year = {2013}
}
@article{cdsos-jlap,
  author = {R. J. Colvin and I. J. Hayes},
  title = {Structural Operational Semantics through Context-Dependent Behaviour},
  journal = {Journal of Logic and Algebraic Programming},
  publisher = {Elsevier},
  volume = {80},
  number = {7},
  doi = {10.1016/j.jlap.2011.05.001},
  pages = {392--426},
  submitted = {25 September 2009},
  revised = {10 May 2011},
  accepted = {Accepted 17 May 2011},
  online = {Available online 30 May 2011},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {LP0989363 BTLink},
  abstract = {We present a new approach to providing a structural operational semantics for imperative
    programming languages with concurrency and procedures. The approach is novel
    because we expose the building block operations—--variable assignment and condition
    checking—--in the labels on the transitions; these form the context-dependent behaviour of
    a program. Using this style results in two main advantages over standard formalisms for imperative
    programming language semantics: firstly, our individual transition rules are more
    concise, and secondly, we are able to more abstractly and intuitively describe the semantics
    of procedures, including by-value and by-reference parameters. Standard techniques in
    the literature tend to result in complex and hard-to-read rules for even simple language
    constructs when procedures and parameters are dealt with. Our semantics for procedures
    utilises the context-dependent behaviour in the transition label to handle variable name
    scoping, and defines the semantics of recursion without requiring additional rules. In contrast
    with Plotkin’s seminal structural operational semantics paper, we do not use locations
    to describe some of the more complex language constructs. Novel aspects of the abstract
    syntax include local states (in contrast to a single global store), which simplifies the reasoning
    about local variables, and a command for dynamically renaming variables (in contrast
    to mapping variables to locations), which simplifies the reasoning about the effect of procedures
    on by-reference parameters.},
  year = {2011}
}
@article{bt-sem-scp,
  author = {R. J. Colvin and I. J. Hayes},
  title = {A Semantics for {Behavior Trees} Using {CSP} with Specification Commands},
  journal = {Science of Computer Programming},
  publisher = {Elsevier},
  volume = {76},
  number = {10},
  doi = {10.1016/j.scico.2010.11.007},
  url = {http://www.sciencedirect.com/science/article/pii/S0167642310002066},
  pages = {891--914},
  issn = {0167-6423},
  accepted = {Accepted 15 Nov 2010},
  online = {Available online 9 December 2010.},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {LP0989363 BTLink},
  abstract = {In this paper we give a formal definition of the requirements translation language Behavior Trees. This
    language has been used with success in industry to systematically translate large, complex, and often
    erroneous requirements documents into a structured model of the system. It contains a mixture of state-based
    manipulations, synchronisation, message passing, and parallel, conditional, and iterative control structures.
    The formal semantics of a Behavior Tree is given via a translation to a version of Hoare's process algebra CSP,
    extended with state-based constructs such as guards and updates, and a message passing facility similar
    to that used in publish/subscribe protocols. We first provide the extension of CSP and its operational
    semantics, which preserves the meaning of the original CSP operators, and then the Behavior Tree notation
    and its translation into the extended version of CSP.},
  keywords = {Structural operational semantics},
  keywords = {Communicating Sequential Processes (CSP)},
  keywords = {Hierarchical state},
  keywords = {Specification commands},
  keywords = {Process algebras},
  keywords = {Behavior Trees},
  keywords = {Requirements modelling},
  year = {2011}
}
@article{ATBFfMRTS,
  author = {Alan Burns and Ian J. Hayes},
  title = {A Timeband Framework for Modelling Real-Time Systems},
  journal = {Real-Time Systems},
  publisher = {Springer Verlag},
  volume = {45},
  number = {1--2},
  pages = {106--142},
  issn = {0922-6443 (Print) 1573-1383 (Online)},
  accepted = {Accepted for publication 19 March 2010},
  online = {Published online 20 April 2010},
  url = {http://www.springerlink.com/content/100334/?Content+Status=Accepted},
  doi = {10.1007/s11241-010-9094-5},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  abstract = {
    Complex real-time systems must integrate physical processes with digital 
    control, human operation and organisational structures. New scientific foundations 
    are required for specifying, designing and implementing these systems. One key
    challenge is to cope with the wide range of time scales and dynamics inherent in such 
    systems. To exploit the unique properties of time, with the aim of producing more 
    dependable computer-based systems, it is desirable to explicitly identify distinct time 
    bands in which the system is situated. Such a framework enables the temporal
    properties and associated dynamic behaviour of existing systems to be described and the 
    requirements for new or modified systems to be specified. A system model based on 
    a finite set of distinct time bands is motivated and developed in this paper.
    },
  keywords = {Real-time systems, time bands},
  month = {June},
  year = {2010}
}
@article{ARfPASaWL,
  author = {Larissa Meinicke and Ian J. Hayes},
  title = {Algebraic reasoning for probabilistic action systems and while-loops},
  journal = {Acta Informatica},
  publisher = {Springer Verlag},
  volume = {45},
  number = {5},
  pages = {321--382},
  issn = {0001-5903},
  accepted = {Accepted for publication 10 March 2008},
  doi = {10.1007/s00236-008-0073-4},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  xrfcd = {280302 (Software Engineering)},
  xseo = {700199 (Computer Software and Services n.e.c.)},
  project = {DP0558408 FTRT},
  abstract = {Back and von Wright have developed algebraic laws for 
    reasoning about 
    loops in a total correctness framework using the refinement
    calculus. We extend their work to reasoning about probabilistic loops
    in the probabilistic refinement calculus. We apply our algebraic
    reasoning to derive transformation rules for probabilistic action
    systems and probabilistic while-loops. In particular we focus on
    developing data refinement rules for these two constructs. Our
    extension is interesting since some well known transformation rules
    that are applicable to standard programs are not applicable to
    probabilistic ones: we identify some of these important differences
    and we develop alternative rules where possible.
    },
  keywords = {Kleene algebra, probability, refinement algebra, total-correctness},
  year = {2008}
}
@article{CMiCLPR,
  author = {R. Colvin and I.J. Hayes and P.A. Strooper},
  title = {Calculating modules in contextual logic program refinement},
  journal = {Theory and Practice of Logic Programming},
  editor = {A. Bossi},
  publisher = {Cambridge University Press},
  doi = {10.1017/S1471068407003043},
  url = {http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=1459272&fulltextType=RA&fileId=S1471068407003043},
  eprint = {http://journals.cambridge.org/article\_S1471068407003043},
  volume = {8},
  number = {01},
  pages = {1--31},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  xrfcd = {280302 (Software Engineering)},
  xseo = {700199 (Computer Software and Services n.e.c.)},
  project = {CEO348249 ACCS/A49937007 RefLP},
  abstract = {
    The refinement calculus for logic programs is a framework for deriving 
    logic programs from specifications.  
    It is based on a wide-spectrum language that
    can express both specifications and code, and a refinement relation that
    models the notion of correct implementation.
    In this paper we extend and generalise earlier work on \emph{contextual
    refinement}.
    Contextual refinement
    simplifies the refinement process by abstractly
    capturing the context of a subcomponent of a program,
    which typically includes information about the values of the 
    free variables.
    This paper also extends and generalises \emph{module refinement}.
    A \emph{module} is a collection of procedures that operate
    on a common data type;
    module refinement between a specification
    module $A$ and an implementation module $C$
    allows calls to the procedures of $A$ to be systematically replaced with
    calls to the corresponding procedures of $C$.
    Based on the conditions for module refinement, we present a method for
    \emph{calculating} an implementation module from a specification module.
    Both contextual and
    module refinement within the refinement calculus have been generalised 
    from earlier work and the results are presented in a unified framework.},
  keywords = {Logic programs, refinement, modules, context},
  year = {2008}
}
@article{PaPitRTPRC,
  author = {I. J. Hayes},
  title = {Procedures and Parameters in the Real-time Program Refinement Calculus},
  journal = {Science of Computer Programming},
  issn = {0167-6423},
  volume = {64},
  number = {3},
  month = {February},
  pages = {286--311},
  doi = {10.1016/j.scico.2006.06.002},
  project = {DP0558408 FTRT/DP0209722 CRTR},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  abstract = {The real-time refinement calculus is a formal method for the
    systematic derivation of real-time programs from real-time
    specifications in a style similar to the non-real-time refinement
    calculi of Back and Morgan.
    In this paper we extend the real-time refinement calculus with
    procedures and provide refinement rules for refining real-time
    specifications to procedure calls.
    A real-time specification can include constraints on, 
    not only what outputs are produced, 
    but also when they are produced.
    The derived programs can also include time constraints on when certain
    points in the program must be reached;
    these are expressed in the form of deadline commands.
    Such programs are machine independent.
    An important consequence of the approach taken is that,
    not only are the specifications machine independent,
    but the whole refinement process is machine independent.
    To implement the machine independent code on a target machine
    one has a separate task of showing that the compiled machine code
    will reach all its deadlines before they expire.

    For real-time programs, externally observable input and output
    variables are essential.
    These differ from local variables in that their values are observable
    over the duration of the execution of the program.
    Hence procedures require input and output parameter mechanisms
    that are references to the actual parameters so that changes to
    external inputs are observable within the procedure and changes to
    output parameters are externally observable.
    In addition, we allow value and result parameters.
    These may be auxiliary parameters,
    which are used for reasoning about the correctness of real-time programs
    as well as in the expression of timing deadlines,
    but do not lead to any code being generated for them by a compiler.
    },
  keywords = {Real-time programming; Procedures and parameters; 
    refinement calculus},
  year = {2007}
}
@article{ZVDM06,
  author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
  journal = {{FACS} {FACTS}},
  pages = {56--78},
  title = {Understanding the differences between {VDM} and {Z}},
  volume = {2006-2},
  year = 2006
}
@article{ATfETDiRTP,
  author = {K. Lermer and C. J. Fidge and I. J. Hayes},
  title = {A Theory for Execution-time Derivation in Real-time Programs},
  journal = {Theoretical Computer Science},
  issn = {0304-3975},
  volume = {346},
  number = {1},
  month = {November},
  pages = {3--27},
  snote = {Special issue on Quantitative Aspects of Programming Languages},
  project = {DP0209722 CRTR},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  year = {2005},
  abstract = {We provide an abstract command language
    for real-time programs and
    outline how a partial correctness semantics
    can be used to
    compute
    execution times.
    The notions of a timed command, refinement of a timed command,
    the command traversal condition,
    and the worst-case and best-case execution time
    of a command are
    formally introduced and investigated with the
    help of an underlying
    weakest liberal precondition semantics.
    The central result is a theory for the computation of worst-case
    and best-case
    execution times from the underlying semantics based
    on supremum and infimum calculations.
    The framework is applied to the
    analysis of a message transmitter
    program
    and its implementation.},
  keywords = {Real-time programming; Control-flow analysis; 
    Execution-time derivation and prediction; 
    Predicate transformer semantics; Partial correctness}
}
@article{LAoETC,
  author = {K. Lermer and C.J. Fidge and I.J. Hayes},
  title = {Linear Approximation of Execution-Time Constraints},
  journal = {Formal Aspects of Computing},
  volume = {15},
  number = {4},
  month = {December},
  pages = {319--348},
  trnumber = {02-31},
  xnote = {in Special Issue on Semantic Foundations of Engineering Design Languages},
  project = {DP0209722 CRTR},
  year = {2003},
  abstract = {This paper defines an algorithm for predicting
    worst-case and best-case execution times, and
    determining execution-time
    constraints of control-flow paths
    through real-time programs using their
    partial correctness
    semantics.
    The algorithm
    produces
    a linear
    approximation of path traversal conditions,
    worst-case and best-case
    execution times and strongest postconditions
    for timed paths in abstract real-time programs.
    We further derive techniques to determine
    the set
    of control-flow paths with
    decidable worst-case and best-case execution times.
    The approach is based on a
    weakest liberal precondition
    semantics
    and relies on supremum and infimum calculations
    similar
    to standard computations from
    linear programming and Presburger
    arithmetic. The methodology is generic in that it is
    applicable to any executable language that
    can be supplied with a predicate
    transformer semantics and hence
    provides a verification
    basis for
    high level as well as assembler level execution-time
    analysis techniques.},
  keywords = {Real-time program analysis; Timing-path analysis;
    Timing prediction; Worst-case and best-case execution times;
    Automatic constraint determination.}
}
@article{aRCfLP,
  author = {I. J. Hayes and R. Colvin and D. Hemer and P. A. Strooper and R. Nickson},
  title = {A Refinement Calculus for Logic Programs},
  journal = {Theory and Practice of Logic Programming},
  volume = {2},
  number = {4--5},
  month = jul,
  dates = {July--September},
  pages = {425--460},
  issn = {?},
  project = {A49937007 RefLP},
  year = {2002},
  abstract = {
    Existing refinement calculi provide frameworks for the stepwise 
    development of imperative programs from specifications.
    This paper presents a refinement calculus for deriving logic programs.
    The calculus contains a wide-spectrum logic programming language, 
    including executable constructs such as sequential conjunction, 
    disjunction, and
    existential quantification, as well as specification constructs
    such as general predicates, assumptions and universal quantification.
    A declarative semantics is defined for this wide-spectrum language 
    based on {\em executions}. 
    Executions are partial functions from states to states,
    where a state is represented as a set of bindings.
    The semantics is used to define the meaning of programs and
    specifications, including parameters and recursion.
    To complete the calculus, a notion of correctness-preserving refinement 
    over programs in the wide-spectrum language is defined
    and refinement laws for developing programs are introduced.
    The refinement calculus is illustrated using example derivations and
    prototype tool support is discussed.}
}
@article{RaRTRTaN,
  title = {Reasoning about Real-Time Repetitions: Terminating and Nonterminating},
  author = {I. J. Hayes},
  journal = {Science of Computer Programming},
  publisher = {Elsevier},
  volume = {43},
  number = {2--3},
  pages = {161--192},
  pdf = {../Papers/iloop.pdf},
  issn = {0167-6423},
  keywords = {Real-time refinement; nonterminating repetitions.},
  url = {http://www.elsevier.com/locate/scico},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {DP0209722 CRTR/A49801500 HertZ},
  year = {2002},
  abstract = {
    It is common for a real-time system to contain a
    nonterminating process monitoring an input and controlling
    an output.  Hence a real-time program development
    method needs to support nonterminating repetitions.
    In this paper we develop a general proof rule for
    reasoning about possibly nonterminating repetitions.
    The rule makes use of a Floyd-Hoare-style loop invariant
    that is maintained by each iteration of the repetition,
    a Jones-style relation between the pre- and post-states on
    each iteration, and a deadline specifying an upper bound
    on the starting time of each iteration.  The general rule
    is proved correct with respect to a predicative semantics.

    In the case of a terminating repetition the rule reduces
    to the standard rule extended to handle real time.
    Other special cases include repetitions whose bodies
    are guaranteed to terminate, nonterminating repetitions
    with the constant true as a guard, and repetitions
    whose termination is guaranteed by the inclusion of a
    fixed deadline.}
}
@article{AItRTOZ,
  author = {G. Smith and I. J. Hayes},
  title = {An Introduction to {Real-Time Object-Z}},
  journal = {Formal Aspects of Computing},
  issn = {0934-5043},
  volume = {13},
  number = {2},
  month = {May},
  pages = {128--141},
  special = {Selected papers from IFM '99},
  publisher = {BCS/Springer-Verlag},
  city = {London},
  project = {DP0209722 CRTR/A49801500 HertZ},
  year = {2002},
  abstract = {
    This paper presents Real-Time Object-Z: an integration of the
    object-oriented, state-based specification language Object-Z with the
    timed trace notation of the timed refinement calculus. This
    integration provides a method of formally specifying and refining
    systems involving continuous variables and real-time constraints. The
    basis of the integration is a mapping of the existing Object-Z
    history semantics to timed traces.},
  keywords = {Real-time specification; real-time refinement; Object-Z; timed
    refinement calculus}
}
@article{SCoDCFP,
  author = {I. J. Hayes and C. J. Fidge and K. Lermer},
  title = {Semantic Characterisation of Dead Control-Flow Paths},
  journal = {IEE Proceedings---Software},
  volume = {148},
  number = {6},
  month = {December},
  pages = {175--186},
  pdf = {../Papers/dead.pdf},
  note = {Awarded the 2001/2002 \emph{Mather Premium} by the Institution of Electrical Engineers},
  project = {A49937045 TPA},
  year = {2001},
  abstract = {
    Many program verification, testing and performance prediction 
    techniques rely on analysis of statically-identified control-flow
    paths. However, some such paths may be `dead' because they can
    never be followed at run time, and should therefore be excluded 
    from analysis.
    It is shown how the formal semantics of those statements comprising
    a path provides a sound theoretical foundation for identification
    of dead paths.}
}
@article{aSRTRC,
  author = {I. J. Hayes and M. Utting},
  title = {A Sequential Real-Time Refinement Calculus},
  journal = {Acta Informatica},
  publisher = {Springer},
  volume = {37},
  number = {6},
  pages = {385--448},
  pdf = {../Papers/srtr.pdf},
  project = {A49801500 HertZ},
  year = {2001},
  abstract = {
    We present a comprehensive refinement calculus for the
    development of sequential, real-time programs from real-time
    specifications.
    A specification may include not only execution time limits,
    but also requirements on the behaviour of outputs over the
    duration of the execution of the program.

    The approach allows refinement steps that separate timing
    constraints and functional requirements.
    New rules are provided for handling timing constraints, but
    the refinement of components implementing functional
    requirements is essentially the same as in the standard
    refinement calculus.

    The product of the refinement process is a program in the
    target programming language extended with timing deadline
    directives. The extended language is a machine-independent,
    real-time programming language.
    To provide valid machine code for a particular model of machine,
    the machine code produced by a compiler must be analysed to
    guarantee that it meets the specified timing deadlines.},
  keywords = {Refinement calculus; machine-independent;
    real-time specification; real-time refinement;
    real-time programming; deadline command; timing constraint analysis;
    time-invariant properties.}
}
@article{TDC,
  author = {C. J. Fidge and I. J. Hayes and G. Watson},
  title = {The Deadline Command},
  journal = {IEE Proceedings---Software},
  volume = {146},
  number = {2},
  month = apr,
  pages = {104--111},
  ps = {../Papers/deadline.ps},
  project = {A49937045 TPA-L},
  year = {1999}
}
@article{aPRT,
  author = {D. Carrington and I. Hayes and R. Nickson and
            G. Watson and J. Welsh},
  title = {A Program Refinement Tool},
  journal = {Formal Aspects of Computing},
  volume = {10},
  number = {2},
  pages = {97--124},
  ps = {../Papers/prtj.ps},
  publisher = {BCS/Springer},
  year = {1998}
}
@article{EPoSL,
  author = {I. J. Hayes},
  title = {Expressive power of specification languages},
  journal = {Formal Aspects of Computing},
  volume = {10},
  number = {2},
  pages = {187--192},
  publisher = {BCS/Springer},
  year = {1998}
}
@article{SCiPR,
  author = {R. Nickson and I. J. Hayes},
  title = {Supporting Contexts in Program Refinement},
  key = {program window inference},
  journal = {Science of Computer Programming},
  uqcall = {QA75.5 .S35},
  volume = {29},
  number = {3},
  pages = {279--302},
  project = {PRT},
  year = {1997},
  abstract = {
    A program can be refined either by transforming the whole program
    or by refining one of its components.  
    The refinement of a component is, for the main part,
    independent of the remainder of the program.
    However, refinement of a component can depend on the 
    {\em context\/} of the component for information about the
    variables that are in scope and what their types are.  
    The refinement can also take advantage of additional information,
    such as any precondition the component can assume.
    
    The aim of this paper is to introduce a technique, which we call
    {\em program window inference\/}, to handle such contextual
    information during derivations in the refinement calculus.
    The idea is borrowed from a technique, called {\em window
    inference\/}, for handling context in theorem proving.
    Window inference is the primary proof paradigm of the {\em Ergo\/}
    proof editor.  This tool has been extended to mechanize refinement
    using program window inference.}
}
@article{Hayes:reuse-mod,
  author = {I. J. Hayes},
  key = {refinement calculus; reuse; module},
  title = {Supporting module reuse in refinement},
  journal = {Science of Computer Programming},
  issn = {0167 6423},
  uqcall = {QA75.5 .S35},
  volume = {27},
  number = {2},
  pages = {175--184},
  year = {1996}
}
@article{HayesSanders:sepio,
  author = {I. J. Hayes and J. W. Sanders},
  title = {Specification by interface separation},
  journal = {Formal Aspects of Computing},
  volume = {7},
  number = {4},
  pages = {430--439},
  pdf = {../Papers/sepio-fac.pdf},
  year = {1995}
}
@article{HayesMahony-units,
  author = {I. J. Hayes and B. P. Mahony},
  title = {Using units of measurement in formal specifications},
  journal = {Formal Aspects of Computing},
  publisher = {BCS/Springer},
  volume = {7},
  number = {3},
  pages = {329--347},
  pdf = {../Papers/units.pdf},
  year = {1995}
}
@article{Diff-VDM-Z-SS,
  author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
  title = {Understanding the differences between {VDM} and {Z}},
  journal = {ACM Software Engineering News},
  publisher = {ACM},
  note = {Unrefereed. Previously published in {\em FACS Europe} \cite{Diff-VDM-Z}},
  volume = {19},
  number = {3},
  pages = {75--81},
  month = {July},
  year = {1994}
}
@article{Diff-VDM-Z,
  author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
  title = {Understanding the differences between {VDM} and {Z}},
  journal = {FACS Europe},
  volume = {1},
  number = {1},
  pages = {7--30},
  note = {Unrefereed. Also published in {\em ACM Software Engineering News}, 19(3):75--81, July 1994},
  dates = {Autumn},
  year = {1993}
}
@article{MahonyHayes:Mine,
  author = {B. P. Mahony and I. J. Hayes},
  title = {A case-study in timed refinement: A mine pump},
  journal = {IEEE Trans.\ on Software Engineering},
  volume = 18,
  number = 9,
  pages = {817--826},
  pdf = {../Papers/mahony92mine.pdf},
  year = {1992}
}
@article{Hayes90f,
  author = {I. J. Hayes},
  title = {{VDM} and {Z}: A comparative case study},
  journal = {Formal Aspects of Computing},
  volume = {4},
  number = {1},
  pages = {76--99},
  pdf = {../Papers/ndb.pdf},
  category = {D},
  year = 1992
}
@article{Hayes89e,
  author = {I. J. Hayes},
  title = {Multi-Relations in {Z}: A cross between multi-sets and binary relations},
  journal = {Acta Informatica},
  volume = {29},
  number = {1},
  pages = {33--62},
  pdf = {../Papers/mrelpap.pdf},
  month = {February},
  category = {D},
  year = 1992
}
@article{HayesJones89,
  author = {I. J. Hayes and C. B. Jones},
  journal = {IEE/BCS Software Engineering Journal},
  month = {November},
  number = {6},
  pages = {330--338},
  title = {Specifications are not (necessarily) executable},
  doi = {10.1049/sej.1989.0045},
  volume = {4},
  year = {1989}
}
@article{HoareHayesEtcFull87,
  author = {C. A. R. Hoare and I. J. Hayes and {He Jifeng} and C. Morgan and A. W. Roscoe and J. W. Sanders and I. H. S{\o}rensen and J. M. Spivey and B. A. Sufrin},
  journal = {Communications of the ACM},
  key = {full},
  month = {August},
  number = {8},
  pages = {672--686},
  title = {Laws of Programming},
  volume = {30},
  note = {Corrigenda: CACM 30(9):770},
  year = {1987}
}
@article{Hayes86a,
  author = {I. J. Hayes},
  howpublished = {PRG-49},
  journal = {IEEE Transactions on Software Engineering},
  key = {abstract data type invariant retrival function Z},
  month = {January},
  number = {1},
  pages = {124--133},
  title = {Specification directed module testing},
  pdf = {../Papers/spectest.pdf},
  volume = {SE-12},
  year = {1986}
}
@article{Hayes85a,
  annote = {Field  Hayes 1985},
  author = {I. J. Hayes},
  journal = {IEEE Transactions on Software Engineering},
  key = {orig Z Language, CICS},
  month = {February},
  number = {2},
  pages = {169--178},
  title = {Applying formal specification to software development in industry},
  pdf = {../Papers/cics-r.pdf},
  volume = {SE-11},
  year = {1985}
}

This file was generated by bibtex2html 1.99.

Last updated: Wed 3 Jan 2024 17:12:52 AEDT