pubs.bib

@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib -ob pubs.bib -oc pubs-cites -c 'not $key : "TRX$"' ../pubs-html.bib}}
@inproceedings{VerifyingCompilerOptimisations,
  author = {Hayes, Ian J. and Utting, Mark and Webb, Brae J.},
  editor = {Li, Yi and Tahar, Sofi\`{e}ne},
  title = {Verifying Compiler Optimisations},
  note = {Invited paper},
  booktitle = {Formal Methods and Software Engineering (ICFEM 2023)},
  conference = {24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, Queensland, Australia, November 21-24, 2023, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {14308},
  publisher = {Springer Nature},
  address = {Singapore},
  pages = {3--8},
  abstract = {Compilers are a vital tool but errors in a compiler can lead to errors in the myriad of programs it compiles. Our research focuses on verifying the optimisation phase because it is a common source of errors within compilers. In programming language semantics, expressions (or terms) are represented by abstract syntax trees, and their semantics is expressed over their (recursive) structure. Optimisations can then be represented by conditional term rewriting rules. The correctness of these rules is verified in Isabelle/HOL. In the GraalVM compiler, the intermediate representation is a sea-of-nodes graph structure that combines data flow and control flow in the one graph. The data flow sub-graphs correspond to term graphs, and the term rewriting rules apply equally to this representation.},
  isbn = {978-981-99-7584-6_1},
  doi = {10.1007/978-981-99-7584-6_1},
  submitted = {Submitted 1 Sep 2023},
  project = {Veriopt},
  year = {2023}
}
@inproceedings{TraceModelsOfCVAs,
  author = {Evangelou-Oost, Naso and Meinicke, Larissa and Bannister, Callum and Hayes, Ian J.},
  editor = {Li, Yi and Tahar, Sofi\`{e}ne},
  title = {Trace Models of Concurrent Valuation Algebras},
  booktitle = {Formal Methods and Software Engineering (ICFEM 2023)},
  conference = {24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, Queensland, Australia, November 21-24, 2023, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {14308},
  publisher = {Springer Nature},
  address = {Singapore},
  pages = {118--136},
  abstract = {This paper introduces Concurrent Valuation Algebras (CVAs), a novel extension of ordered valuation algebras (OVAs). CVAs include two combine operators representing parallel and sequential prod- ucts, adhering to a weak exchange law. This development offers theoret- ical and practical benefits for the specification and modelling of concur- rent and distributed systems. As a presheaf on a space of domains, CVAs enable localised specifications, supporting modularity, compositionality, and the ability to represent large and complex systems. Furthermore, CVAs align with lattice-based refinement reasoning and are compatible with established methodologies such as Hoare and Rely-Guarantee logics. The flexibility of CVAs is explored through three trace models, illustrat- ing distinct paradigms of concurrent/distributed computing, interrelated by morphisms. The paper also highlights the potential to incorporate a powerful local computation framework from valuation algebras for model checking in concurrent and distributed systems. The foundational results presented have been verified with the proof assistant Isabelle/HOL.},
  isbn = {978-981-99-7584-6_8},
  doi = {10.1007/978-981-99-7584-6_8},
  submitted = {Submitted 31 May 2023},
  accepted = {Accepted 31 July 2023},
  project = {DP190102142 DV4CS},
  year = {2023}
}
@inproceedings{Jifeng_festschrift23,
  author = {Hayes, Ian J. and Jones, Cliff B. and Meinicke, Larissa A.},
  editor = {Bowen, Jonathan P. and Li, Qin and Xu, Qiwen},
  title = {Specifying and reasoning about shared-variable concurrency},
  booktitle = {Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday},
  series = {Lecture Notes in Computer Science},
  volume = {14080},
  publisher = {Springer Nature Switzerland AG},
  address = {Cham},
  pages = {110--135},
  abstract = {Specifications are a necessary reference point for correctness arguments. Top-down descriptions of concurrent programs require a way of recording information about the environment in which the component will be required to function. It was shown in the 1980s that adding rely and guarantee conditions to pre and post conditions could support formal specification and reasoning about a class of concurrent systems. More recent research has both widened the class of specifications to include progress requirements and facilitated mechanisation of proofs. This paper describes the algebraic underpinnings that have made this possible. Particular attention is paid to notions of atomicity.},
  isbn = {978-3-031-40436-8_5},
  doi = {10.1007/978-3-031-40436-8_5},
  submitted = {Submitted 20 March 2023},
  accepted = {Accepted 8 April 2023},
  project = {DP190102142 DV4CS},
  year = {2023}
}
@inproceedings{FormaliSE_localisation,
  title = {Using cylindric algebra to support local variables in rely/guarantee concurrency},
  author = {Meinicke, Larissa A. and Hayes, Ian J.},
  doi = {10.1109/FormaliSE58978.2023.00019},
  abstract = {Local variable blocks are a simple but effective program structuring technique.
                In the context of concurrency,
                local variables have the added advantage of avoiding interference
                from threads running concurrently with the thread containing the local variable.
                To provide mechanised support for verifying concurrent programs in Isabelle/HOL,
                we have found making use of algebraic properties of programs
                simplifies the development of refinement laws.
                The algebraic properties of local variable blocks are similar to
                those of existential quantifiers in predicate calculus,
                the algebra of which is Tarski's cylindric algebra.
                Hence to support local variables, we make use of a variant of cylindric algebra
                that allows quantification of a variable over a command, rather than a predicate.
                The approach allows a local variable to become a shared variable of parallel threads
                that are local to the block that introduced the variable.},
  booktitle = {2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE)},
  conference = {FormaliSE 2023},
  location = {Melbourne, Australia},
  publisher = {IEEE},
  pages = {108-119},
  keywords = {Rely/guarantee concurrency, Concurrent program verification, Program algebra,
                Cylindric algebra, Local variables},
  submitted = {Submitted 28 Jan 2023},
  accepted = {Accepted 22 Feb 2023},
  project = {DP190102142 DV4CS},
  year = 2023
}
@inproceedings{veriopt:validation,
  title = {Differential Testing of a Verification Framework for Compiler Optimizations (Case Study)},
  author = {Utting, Mark and Webb, Brae J. and Hayes, Ian J.},
  abstract = {We want to verify the correctness of optimization phases in the GraalVM compiler,
                which consist of many thousands of lines of complex Java code
                performing sophisticated graph transformations.
                We have built high-level models of the data structures and
                operations of the code using the Isabelle/HOL theorem prover,
                and can formally verify the correctness of those high-level operations. 
                But the remaining challenge is: how can we be sure
                that those high-level operations accurately reflect what the Java is doing? 
                This paper addresses that issue by applying several different kinds of differential testing
                to validate that the formal model and the Java code have the same semantics.
                The lessons learned from applying these validation techniques should be applicable to
                other projects that are building formal models of real-world code.},
  booktitle = {FormaliSE 2023},
  conference = {FormaliSE 2023},
  location = {Melbourne, Australia},
  publisher = {IEEE},
  keywords = {
          Logic in Computer Science (cs.LO), Programming Languages (cs.PL), Software
          Engineering (cs.SE), FOS: Computer and information sciences, FOS: Computer
          and information sciences
  },
  submitted = {Submitted 28 Jan 2023},
  accepted = {Accepted 22 Feb 2023},
  project = {Veriopt},
  year = 2023
}
@inproceedings{ContextualityInDistributedSystems,
  author = {Evangelou-Oost, Nasos and Bannister, Callum and Hayes, Ian J.},
  editor = {Gl{\"u}ck, Roland and Santocanale, Luigi and Winter, Michael},
  title = {Contextuality in Distributed Systems},
  booktitle = {Relational and Algebraic Methods in Computer Science},
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {52--68},
  abstract = {We present a lattice of distributed program specifications, whose ordering represents implementability/refinement. Specifications are modelled by families of subsets of relative execution traces, which encode the local orderings of state transitions, rather than their absolute timing according to a global clock. This is to overcome fundamental physical difficulties with synchronisation. The lattice of specifications is assembled and analysed with several established mathematical tools. Sets of nondegenerate cells of a simplicial set are used to model relative traces, presheaves model the parametrisation of these traces by a topological space of variables, and information algebras reveal novel constraints on program correctness. The latter aspect brings the enterprise of program specification under the widening umbrella of contextual semantics introduced by Abramsky et al. In this model of program specifications, contextuality manifests as a failure of a consistency criterion comparable to Lamport's definition of sequential consistency. The theory of information algebras also suggests efficient local computation algorithms for the verification of this criterion. The novel constructions in this paper have been verified in the proof assistant Isabelle/HOL.},
  isbn = {978-3-031-28083-2},
  doi = {10.1007/978-3-031-28083-2_4},
  submitted = {Submitted 15 Oct 2022},
  accepted = {Accepted 17 Dec 2022},
  project = {DP190102142 DV4CS},
  year = {2023}
}
@inproceedings{TermGraphOptimizations,
  author = {Webb, Brae J. and Hayes, Ian J. and Utting, Mark},
  title = {Verifying Term Graph Optimizations Using {Isabelle/HOL}},
  isbn = {9798400700262},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3573105.3575673},
  doi = {10.1145/3573105.3575673},
  abstract = {Our objective is to formally verify the correctness of the hundreds of expression optimization rules
    used within the GraalVM compiler.
    When defining the semantics of a programming language, expressions naturally form abstract syntax trees, or, terms.
    However, in order to facilitate sharing of common subexpressions,
    modern compilers represent expressions as term graphs.
    Defining the semantics of term graphs is more complicated than
    defining the semantics of their equivalent term representations.
    More significantly, defining optimizations directly on term graphs and
    proving semantics preservation is considerably more complicated than on the equivalent term representations.
    On terms, optimizations can be expressed as conditional term rewriting rules,
    and proofs that the rewrites are semantics preserving are relatively straightforward.
    In this paper, we explore an approach to using term rewrites to verify term graph transformations
    of optimizations within the GraalVM compiler.
    This approach significantly reduces the overall verification effort and
    allows for simpler encoding of optimization rules.},
  booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  pages = {320--333},
  numpages = {14},
  keywords = {sea-of-nodes intermediate representation, GraalVM compiler, verified code optimizer, Isabelle/HOL},
  location = {Boston, MA, USA},
  series = {CPP 2023},
  submitted = {Submitted 22 Sep 2022},
  accepted = {Accepted 22 Nov 2022},
  project = {Veriopt},
  year = {2023}
}
@inproceedings{SoftwareSpecificationTony21,
  author = {Hayes, Ian J. and King, Steve},
  title = {Software Specification},
  isbn = {9781450387286},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  edition = {1},
  url = {https://doi.org/10.1145/3477355.3477367},
  booktitle = {Theories of Programming: The Life and Works of Tony Hoare},
  editor = {Jones, Cliff B. and Misra, Jayadev},
  pages = {251–270},
  numpages = {20},
  project = {DP190102142 DV4CS},
  year = {2021}
}
@inproceedings{ATVA21_GraalVM_IR_Semantics,
  author = {Webb, Brae J. and Utting, Mark and Hayes, Ian J.},
  editor = {Hou, Zhe and Ganesh, Vijay},
  title = {A Formal Semantics of the {GraalVM} Intermediate Representation},
  booktitle = {Automated Technology for Verification and Analysis},
  conference = {19th International Symposium on Automated Technology for Verification and Analysis (ATVA 2021), 18-22 October 2021, Gold Coast (Online), Australia},
  pages = {111--126},
  series = {Lecture Notes in Computer Science},
  volume = {12971},
  publisher = {Springer International Publishing},
  address = {Cham},
  issn = {0302-9743},
  isbn = {978-3-030-88885-5},
  doi = {10.1007/978-3-030-88885-5_8},
  submitted = {Submitted 24 April 2021},
  accepted = {Accepted 5 June 2021},
  online = {Online ??},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {Veriopt},
  abstract = {The optimization phase of a compiler is responsible for
transforming an intermediate representation (IR) of a program into a more efficient form.
Modern optimizers, such as that used in the GraalVM compiler,
use an IR consisting of a sophisticated graph data structure
that combines data flow and control flow into the one structure.
As part of a wider project on the verification of optimization passes of GraalVM,
this paper describes a semantics for its IR within Isabelle/HOL.
The semantics consists of a big-step operational semantics for data nodes
(which are represented in a graph-based static single assignment (SSA) form)
and a small-step operational semantics for handling control flow
including heap-based reads and writes, exceptions, and method calls.
We have proved a suite of canonicalization optimizations and
conditional elimination optimizations with respect to the semantics.},
  month = oct,
  year = {2021}
}
@misc{hayes2021deriving,
  title = {Deriving Laws for Developing Concurrent Programs in a Rely-Guarantee Style},
  author = {Ian J. Hayes and Larissa A. Meinicke and Patrick A. Meiring},
  eprint = {2103.15292},
  note = {Ext. report at \href{http://arxiv.org/abs/2103.15292}{arXiv:2103.15292}},
  archiveprefix = {arXiv},
  primaryclass = {cs.LO},
  url = {https://arxiv.org/abs/2103.15292},
  project = {DP190102142 DV4CS},
  year = {2021}
}
@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}
}
@inproceedings{UTP19,
  author = {I. J. Hayes and L. A. Meinicke},
  title = {Developing an algebra for rely/guarantee concurrency: design decisions and challenges},
  booktitle = {Unifying Theories of Programming 2019},
  editor = {Pedro Ribeiro and Augusto Sampaio},
  pages = {176--197},
  note = {},
  series = {Lecture Notes in Computer Science},
  volume = {11885},
  publisher = {Springer International Publishing},
  address = {Cham},
  issn = {0302-9743},
  doi = {10.1007/978-3-030-31038-7_9},
  submitted = {Submitted 24 May 2019},
  accepted = {Accepted 25 June 2019},
  online = {Online ??},
  optkey = {},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP190102142 DV4CS},
  abstract = {An algebra for rely/guarantee concurrency has beenc onstructed via a
                  hierarchy of algebraic theories starting from basic theories like lattices through to
                  theories of synchronous behaviour of atomic steps and a theory to support localisation.
                  The algebra is supported by a model based on Aczel traces.
                  We examine the role of these theories in developing a mechanised theory
                  for deriving concurrent programs and outline some of the challenges remaining.
                 },
  month = oct,
  year = {2019},
  optannote = {}
}
@inproceedings{MPC19CylindricAlgebra,
  author = {B. Dongol and I. J. Hayes and L. A. Meinicke and G. Struth},
  title = {Cylindric {Kleene} Lattices for Program Construction},
  booktitle = {Mathematics of Program Construction 2019},
  editor = {G. Hutton},
  pages = {197--225},
  note = {},
  series = {Lecture Notes in Computer Science},
  volume = {11825},
  publisher = {Springer International Publishing},
  address = {Cham},
  issn = {0302-9743},
  isbn = {978-3-030-33636-3},
  doi = {10.1007/978-3-030-33636-3_8},
  submitted = {Submitted 11 May 2019},
  accepted = {Accepted 14 June 2019},
  online = {Online ??},
  optkey = {},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP190102142 DV4CS},
  abstract = {Cylindric algebras have been developed as an algebraisation of
                  equational first order logic.  We adapt them to cylindric Kleene
                  lattices and their variants and present relational and relational
                  fault models for these. This allows us to encode frames and local
                  variable blocks, and to derive Morgan's refinement calculus as well
                  as an algebraic Hoare logic for while programs with assignment
                  laws. Our approach thus opens the door for algebraic calculations
                  with program and logical variables instead of domain-specific
                  reasoning over concrete models of the program store. Refinement
                  proofs for small programs are presented as examples.
                 },
  year = {2019},
  optannote = {}
}
@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}
}
@inproceedings{SETSS17-proc,
  author = {I. J. Hayes and C. B. Jones},
  title = {A Guide to Rely/Guarantee Thinking},
  booktitle = {Engineering Trustworthy Software Systems},
  editor = {J. P. Bowen and Z. Liu and Z. Zhang},
  pages = {1--38},
  note = {},
  series = {Lecture Notes in Computer Science},
  volume = {11174},
  publisher = {Springer International Publishing},
  address = {Cham},
  issn = {0302-9743},
  isbn = {978-3-030-02927-2},
  doi = {10.1007/978-3-030-02928-9},
  submitted = {Submitted ?? Dec 2017},
  accepted = {Accepted ??},
  online = {Online ??},
  optkey = {},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  abstract = {Designing concurrent shared-variable programs is difficult.
                  The Rely-Guarantee concept provides a compositional approach to the challenge.
                  This paper reviews some recent developments in the approach,
                  offers worked examples and relates the approach to other research.
                 },
  year = {2018},
  optannote = {}
}
@inproceedings{icfem-invited-2018,
  author = {I. J. Hayes},
  title = {Engineering a theory of concurrent programming},
  booktitle = {Formal Methods and Software Engineering (ICFEM)},
  conference = {ICFEM 2018: 20th International Conference on Formal Engineering Methods,
                  Gold Coast, Queensland, Australia, November 12--16, 2018, Proceedings},
  editor = {Jing Sun and Meng Sun},
  pages = {3--18},
  series = {Lecture Notes in Computer Science},
  volume = {11232},
  publisher = {Springer International Publishing},
  address = {Cham},
  issn = {0302-9743},
  isbn = {978-3-030-02449-9},
  doi = {10.1007/978-3-030-02450-5_1},
  note = {Invited keynote paper},
  optkey = {},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP190102142 DV4CS},
  abstract = {Our original goal was to develop a refinement calculus for shared-memory concurrent programs 
                  to support Jones-style rely/guarantee developments. 
                  Our semantics was based on Aczel traces, 
                  which explicitly include environment steps as well as program steps, 
                  and were originally proposed as a basis for showing the rely/guarantee rules are sound. 
                  Where we have ended up is with a hierarchy of algebraic theories 
                  that provide a foundation for concurrent program refinement, 
                  which allows us to prove Jones-style rely/guarantee laws, as well as new laws. 
                  Our algebraic theory is based on a lattice of commands 
                  that includes a sub-lattice of test commands (similar to Kozen's Kleene Algebra with Tests) 
                  and a sub-algebra of atomic step commands (similar to Milner's SCCS) 
                  but with a structure that supports Aczel's program and environment steps as atomic step commands. 
                  The latter allows us to directly encode rely and guarantee commands to represent 
                  rely/guarantee specifications, and to encode fair execution of a command.},
  month = {November},
  year = {2018},
  optannote = {}
}
@inproceedings{lp14-TS4cap-ICFEM-2018,
  author = {X. Wu and Y. Lu and P. Meiring and I. J. Hayes and L. A. Meinicke},
  title = {Type capabilities for object-oriented programming languages},
  booktitle = {Formal Methods and Software Engineering (ICFEM)},
  conference = {ICFEM 2018: 20th International Conference on Formal Engineering Methods,
                  Gold Coast, Queensland, Australia, November 12--16, 2018, Proceedings},
  editor = {Jing Sun and Meng Sun},
  pages = {215--230},
  series = {Lecture Notes in Computer Science},
  volume = {11232},
  publisher = {Springer International Publishing},
  address = {Cham},
  issn = {0302-9743},
  isbn = {978-3-030-02449-9},
  doi = {10.1007/978-3-030-02449-9},
  submitted = {Submitted 2018},
  accepted = {Accepted 2018},
  online = {Online ??},
  optkey = {},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {LP140100700},
  abstract = {},
  month = {November},
  year = {2018},
  optannote = {}
}
@inproceedings{REFINE2018,
  author = {Ian J. Hayes},
  title = {Some Challenges of Specifying Concurrent Program Components},
  booktitle = {{\rm Proceedings}
                  18th Refinement Workshop,
                  {\rm Oxford, UK, 18th July 2018}},
  editor = {Derrick, John and Dongol, Brijesh and Reeves, Steve},
  pages = {10-22},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = {282},
  publisher = {Open Publishing Association},
  doi = {10.4204/EPTCS.282.2},
  submitted = {Submitted 23 April 2018},
  accepted = {Accepted ??? 2018},
  online = {Online 28th October 2018},
  optkey = {},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP190102142 DV4CS},
  abstract = {The purpose of this paper is to address some of the challenges of
                  formally specifying components of shared-memory concurrent programs.
                  The focus is to provide an abstract specification of a component
                  that is suitable for use both by clients of the component and
                  as a starting point for refinement to an implementation of the component.
                  We present some approaches to devising specifications,
                  investigating different forms suitable for different contexts.
                  We examine handling atomicity of access to data structures,
                  blocking operations and progress properties,
                  and transactional operations that may fail and need to be retried.},
  month = {October},
  year = {2018},
  optannote = {}
}
@inproceedings{FM2018fairness,
  author = {I. J. Hayes and L. A. Meinicke},
  title = {Encoding fairness in a synchronous concurrent program algebra},
  booktitle = {Formal Methods},
  conference = {FM 2018: Formal Methods: 22nd International Symposium, Oxford, UK, July 15-17, 2018, Proceedings},
  editor = {Havelund, Klaus and Peleska, Jan and Roscoe, Bill and de Vink, Erik},
  pages = {222--239},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer International Publishing},
  address = {Cham},
  issn = {0934-5043},
  isbn = {978-3-319-95582-7},
  doi = {10.1007/978-3-319-95582-7_13},
  submitted = {Submitted 23 Jan 2018},
  accepted = {Accepted 9 April 2018},
  online = {Online ??},
  optkey = {},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP190102142 DV4CS},
  abstract = {Concurrent program refinement algebra provides a suitable basis for supporting mechanised reasoning about shared-memory concurrent programs in a compositional manner, for example, it supports the rely/guarantee approach of Jones. The algebra makes use of a synchronous parallel operator motivated by Aczel?s trace model of concurrency and with similarities to Milner?s SCCS. This paper looks at defining a form of fairness within the program algebra. The encoding allows one to reason about the fair execution of a single process in isolation as well as define fair-parallel in terms of a base parallel operator, of which no fairness properties are assumed. An algebraic theory to support fairness and fair-parallel is developed.},
  month = {July},
  year = {2018},
  optannote = {}
}
@misc{FM2018fairness-TR,
  author = {Ian J. Hayes and Larissa A. Meinicke},
  title = {Encoding fairness in a synchronous concurrent program algebra: extended version with proofs},
  eprint = {1805.01681},
  archiveprefix = {arXiv},
  primaryclass = {cs.LO},
  url = {https://arxiv.org/abs/1805.01681},
  month = {May},
  project = {DP190102142 DV4CS},
  year = {2018}
}
@misc{FMJournalAtomicSteps-TR,
  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},
  eprint = {1710.03352},
  archiveprefixi = {arXiv},
  primaryclass = {cs.LO},
  url = {https://arxiv.org/abs/1710.03352},
  project = {DP190102142 DV4CS},
  note = {\url{https://arxiv.org/abs/1710.03352}},
  year = {2017}
}
@inproceedings{APLAS17,
  author = {Hayes, Ian J. and Wu, Xi and Meinicke, Larissa A.},
  editor = {Chang, Bor-Yuh Evan},
  title = {Capabilities for {Java}: Secure Access to Resources},
  booktitle = {Programming Languages and Systems: 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings},
  publisher = {Springer International Publishing},
  address = {Cham},
  doi = {10.1007/978-3-319-71237-6_4},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {LP140100700},
  pages = {67--84},
  abstract = {This paper explores adding capabilities to Java with the objective of tightening security management for access to resources both within the Java Class Library and Java applications. Code can only access resources if it is given explicit capabilities, allowing replacement of the use of doPrivileged blocks. Capabilities provide restricted access to their implementing object -- like an interface -- but when a capability is created, it has a more restrictive dynamic type than its implementing object, and hence access to the full facilities of the implementing object (e.g. via down casting) are precluded. We used the Annotation Processing Tool to track the declaration and use of capabilities.},
  isbn = {978-3-319-71237-6},
  doi = {10.1007/978-3-319-71237-6_4},
  url = {https://doi.org/10.1007/978-3-319-71237-6_4},
  year = {2017}
}
@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
}
@inproceedings{FM2016atomicSteps,
  author = {I. J. Hayes and R. Colvin and L. 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 = {J. Fitzgerald and C. Heitmeyer and S. Gnesi and A. Philippou},
  pages = {352--369},
  note = {Best paper award},
  series = {Lecture Notes in Computer Science},
  volume = {9995},
  publisher = {Springer International Publishing},
  address = {Cham},
  issn = {0934-5043},
  isbn = {978-3-319-48989-6},
  doi = {10.1007/978-3-319-48989-6_22},
  url = {http://dx.doi.org/10.1007/978-3-319-48989-6_22},
  submitted = {Submitted ?? 2016},
  accepted = {Accepted 9 August 2016},
  online = {Online ??},
  optkey = {},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  abstract = {This research started with 
    an algebra for reasoning about rely/guarantee concurrency for a shared
    memory model. The approach taken led to a more \emph{abstract algebra of
    atomic steps}, in which atomic steps synchronise (rather than
    interleave) when composed in parallel. The algebra of rely/guarantee
    concurrency then becomes an interpretation of the more abstract
    algebra. Many of the core properties needed for rely/guarantee
    reasoning can be shown to hold in the abstract algebra where their
    proofs are simpler and hence allow a higher degree of
    automation. Moreover, the realisation that the synchronisation
    mechanisms of standard process algebras, such as CSP and CCS/SCCS, can
    be interpreted in our abstract algebra gives evidence of its unifying
    power. The algebra has been encoded in Isabelle/HOL to provide a basis
    for tool support.},
  month = {November},
  year = {2016},
  optannote = {}
}
@misc{FM2016atomicSteps-TR,
  author = {I. J. Hayes and R. Colvin and L. Meinicke and K. Winter and A. Velykis},
  title = {An algebra of synchronous atomic steps},
  eprint = {1609.00118},
  pages = {1--22},
  archiveprefix = {arXiv},
  primaryclass = {cs.LO},
  url = {https://arxiv.org/abs/1609.00118},
  note = {\url{http://dx.doi.org/10.1007/978-3-319-48989-6_22}},
  submitted = {Submitted ?? 2016},
  accepted = {Accepted 9 August 2016},
  online = {Online ??},
  optkey = {},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  abstract = {This research started with
    an algebra for reasoning about rely/guarantee concurrency for a shared
    memory model. The approach taken led to a more \emph{abstract algebra of
    atomic steps}, in which atomic steps synchronise (rather than
    interleave) when composed in parallel. The algebra of rely/guarantee
    concurrency then becomes an interpretation of the more abstract
    algebra. Many of the core properties needed for rely/guarantee
    reasoning can be shown to hold in the abstract algebra where their
    proofs are simpler and hence allow a higher degree of
    automation. Moreover, the realisation that the synchronisation
    mechanisms of standard process algebras, such as CSP and CCS/SCCS, can
    be interpreted in our abstract algebra gives evidence of its unifying
    power. The algebra has been encoded in Isabelle/HOL to provide a basis
    for tool support.},
  month = {November},
  year = {2016},
  optannote = {}
}
@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}
}
@misc{AFfGRGRACP-TR,
  author = {Ian J. Hayes},
  title = {Generalised rely-guarantee concurrency: An algebraic foundation},
  eprint = {1603.01776},
  archiveprefix = {arXiv},
  primaryclass = {cs.LO},
  url = {https://arxiv.org/abs/1603.01776},
  pages = {1--23},
  note = {\url{http://dx.doi.org/10.1007/s00165-012-??-1}},
  submitted = {Submitted 22 April 2014},
  accepted = {Accepted ??},
  online = {Online ??},
  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.
  },
  year = {2015}
}
@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}
}
@inproceedings{SCoRaGiCPD,
  author = {Ian J. Hayes},
  affiliation = {School of Information Technology and Electrical Engineering, The University of Queensland, Australia},
  title = {Separating concerns of rely and guarantee in concurrent program derivation},
  booktitle = {Unifying Theories of Programming, UTP 2014},
  note = {Invited keynote},
  conference = {Singapore, 13 May, 2014},
  editor = {David A. Naumann},
  pages = {vii--x},
  series = {LNCS},
  volume = {8963},
  isbn = {978-3-319-14805-2},
  issn = {0302-9743},
  publisher = {Springer},
  city = {Switzerland},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  keywords = {},
  abstract = {To reason compositionally about concurrent programs one needs to be able to reason 
    about a process in the context of the interference from its environment.  
    Cliff Jones introduced an elegant approach to handle reasoning about interference in terms of 
    rely and guarantee conditions, each of which is a binary relation between program states. 

    In order to provide a unifying theory of rely-guarantee reasoning,
    here guarantees and relies are treated as separate forms of specifications
    in a wide-spectrum language with a single refinement relation.
    The separate forms of specification allow guarantees and relies 
    to be examined separately, leading to simpler expression of their algebraic properties,
    as well as in combination,
    as needed to handle the introduction of a parallel composition.},
  year = {2015}
}
@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}
}
@inproceedings{IWfSaRtPA,
  author = {Ian J. Hayes and Larissa Meinicke},
  affiliation = {School of Information Technology and Electrical Engineering, The University of Queensland, Australia},
  title = {Invariants, Well-founded Statements and Real-time Program Algebra},
  booktitle = {Formal Methods (FM 2014)},
  conference = {Singapore, 12-16 May, 2014},
  accepted = {Accepted 1 Feb 2014},
  editor = {Cliff. B. Jones and P. Pihlajasaari and Jun Sun},
  pages = {318--334},
  series = {LNCS},
  volume = {8442},
  isbn = {978-3-319-06409-3},
  issn = {0302-9743},
  publisher = {Springer},
  city = {Berlin / Heidelberg},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  keywords = {},
  abstract = {Program algebras based on Kleene algebra abstract the essential properties of programming languages in the form of algebraic laws. The proof of a refinement law may be expressed in terms of the algebraic properties of programs required for the law to hold, rather than directly in terms of the semantics of a language. This has the advantage that the law is then valid for any programming language that satisfies the axioms of the algebra.
In this paper we explore the notion of well-founded statements and their relationship to well-founded relations and iterations. The laws about well-founded statements and relations are combined with invariants to derive a simpler proof of a while-loop introduction law.
The algebra is then applied to a real-time programming language. The main difference is that tests within conditions and loops take time to evaluate and during that time the values of program inputs may change. This requires new definitions for conditionals and while loops but the proofs of the introduction laws for these constructs can still make use of the more basic algebraic properties of iterations.},
  year = {2014}
}
@inproceedings{FTSCS13,
  author = {Ian J. Hayes},
  affiliation = {School of Information Technology and Electrical Engineering, The University of Queensland, Australia},
  title = {Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions},
  booktitle = {Formal Techniques for Safety-Critical Systems},
  conference = {Formal Techniques for Safety-Critical Systems: Second International Workshop, FTSCS 2013, Queenstown, New Zealand, October 29-30, 2013. Revised Selected Papers},
  editor = {C. Artho and P.C. \"{O}lveczky},
  pages = {1--2},
  series = {Communications in Computer and Information Science},
  volume = {419},
  isbn = {978-3-319-05415-5},
  publisher = {Springer},
  doi = {10.1007/978-3-319-05416-2_1},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT},
  keywords = {?},
  abstract = {The overall specification of a cyber-physical system can be given in terms of
    the desired behaviour of its physical components operating within the real world.
    The specification of its control software can then be derived
    from the overall specification and the properties of the real-world phenomena,
    including their relationship to the computer system's sensors and actuators.
    The control software specification then becomes a combination of 
    the guarantee it makes about the system behaviour and 
    the real-world assumptions it relies upon.

    Such specifications can easily become complicated because 
    the complete system description deals with 
    properties of phenomena at widely different time granularities, 
    as well as handling faults.
    To help manage this complexity, 
    we consider layering the specification within multiple time bands, 
    with the specification of each time band consisting of both the
    rely and guarantee conditions for that band, 
    both given in terms of the phenomena of that band.
    The overall specification is then the combination of the multiple
    rely-guarantee pairs.
    Multiple rely-guarantee pairs can also be used to handle faults.},
  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
}
@techreport{HayesJonesColvin14TR,
  author = {Ian J. Hayes and Cliff B. Jones and Robert J. Colvin},
  title = {Laws and Semantics for Rely-Guarantee Refinement},
  institution = {School of Computing Science, Newcastle University},
  numpages = {66},
  note = {Superseded by \cite{FMJournalAtomicSteps-TR} and other papers. 66 pages},
  number = {CS-TR-1425},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT/LP0989643 SPA},
  keywords = {rely-guarantee, concurrency},
  abstract = {
    Interference is the essence of concurrency and it is what makes reasoning about concurrent programs difficult.
    The fundamental insight of rely-guarantee thinking is that stepwise design of concurrent programs can only be
    compositional in development methods that offer ways to record and reason about interference.
    In this way of thinking, a rely relation records assumptions about the behaviour of the environment,
    and a guarantee relation records commitments about the behaviour of the process.
    The standard application of these ideas is in the extension of Hoare-like inference rules to quintuples
    that accommodate rely and guarantee conditions.
    In contrast, in this paper, we embed rely-guarantee thinking into a refinement calculus for concurrent programs,
    in which programs are developed in (small) steps from an abstract specification.
    As is usual, we extend the implementation language with specification constructs
    (the extended language is sometimes called a wide-spectrum language),
    in this case adding two new commands:
      a guarantee command $(\mathbf{guar} g ~\cdot~c)$ whose valid behaviours are in accord with the command $c$
      but all of whose atomic steps also satisfy the relation $g$,
      and a rely command $(\mathbf{rely} r ~\cdot~c)$ whose behaviours are like $c$ provided
      any interference steps from the environment satisfy the relation $r$.
      The theory of concurrent program refinement is based on a theory of atomic program steps and
      more powerful refinement laws, most notably,
      a law for decomposing a specification into a parallel composition,
      are developed from a small set of more primitive lemmas,
      which are proved sound with respect to an operational semantics.
  },
  month = jul,
  year = {2014}
}
@inproceedings{PSDFAS,
  author = {Kirsten Winter and Chenyi Zhang and Ian J. Hayes and Nathan Keynes and Cristina Cifuentes and Lian Li},
  affiliation = {School of Information Technology and Electrical Engineering, The University of Queensland, Australia},
  title = {Path-Sensitive Data Flow Analysis Simplified},
  booktitle = {Formal Methods and Software Engineering: Proceedings 15th International Conference on Formal Engineering Methods (ICFEM)},
  conference = {Queenstown, New Zealand, 29 October - 1 November, 2013},
  accepted = {Accepted 19 June 2013},
  editor = {Lindsay Groves and Jing Sun},
  pages = {415--430},
  series = {LNCS},
  volume = {8144},
  isbn = {978-3-642-41201-1},
  issn = {0302-9743},
  publisher = {Springer},
  city = {Berlin / Heidelberg},
  doi = {10.1007/978-3-642-41202-8_27},
  url = {http://dx.doi.org/10.1007/978-3-642-41202-8_27},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  era = {ERA 2012 Listed},
  project = {LP0989643 SPA},
  keywords = {static program analysis},
  abstract = {Path-sensitive data flow analysis pairs classical data flow analysis with an analysis of feasibility of paths to improve precision. In this paper we propose a framework for path-sensitive backward data flow analysis that is enhanced with an abstraction of the predicate domain. The abstraction is based on a three-valued logic. It follows the strategy that path predicates are simplified if possible (without calling an external predicate solver) and every predicate that could not be reduced to a simple predicate is abstracted to the unknown value, for which the feasibility is undecided. The implementation of the framework scales well and delivers promising results.},
  year = {2013}
}
@inproceedings{Visuocode13,
  author = {Daniel R. Bradley and Ian J. Hayes},
  affiliation = {School of Information Technology and Electrical Engineering, The University of Queensland, Australia},
  title = {Visuocode: {A} software development environment that supports spatial navigation and composition},
  booktitle = {First {IEEE} Working Conference on Software Visualization (VISSOFT)},
  conference = {Eindhoven, The Netherlands. 27--28 September, 2013},
  editor = {Alexandru Telea and Andreas Kerren and Andrian Marcus},
  accepted = {Accepted 20 July 2013},
  pages = {1--4},
  isbn = {9781479914579},
  publisher = {IEEE},
  city = {??},
  isbn = {978-1-4799-1457-9},
  doi = {10.1109/VISSOFT.2013.6650533},
  url = {http://dx.doi.org/10.1109/VISSOFT.2013.6650533},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  era = {ERA 2010 Rank B},
  project = {LP0989643 SPA},
  keywords = {program visualisation},
  abstract = {Navigating through software is an integral part of software development. Studies have identified that during navigation programmers often become disoriented and lose task awareness. To mitigate this, the method-flow visualisation technique displays traversed methods in adjacent editor columns. This paper presents the Visuocode software development environment, which is an implementation of method-flow that, in addition to navigation, supports program composition.},
  year = {2013}
}
@techreport{RRGT-TR13,
  author = {Ian J. Hayes and Cliff B. Jones and Robert J. Colvin},
  title = {Reasoning about concurrent programs: Refining rely-guarantee thinking},
  institution = {School of Computing Science, Newcastle University},
  numpages = {66},
  note = {Superseded by CS-TR-1425. 66 pages},
  number = {CS-TR-1395},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT/LP0989643 SPA},
  keywords = {rely-guarantee, concurrency},
  abstract = {
    Interference is the essence of concurrency and it is what makes
    reasoning about concurrent programs difficult.
    The fundamental insight of rely-guarantee thinking is that stepwise design of 
    concurrent programs can only be compositional in development methods that
    offer ways to record and reason about interference.
    In this way of thinking, a \emph{rely} relation records assumptions about
    the behaviour of the \emph{environment}, and a \emph{guarantee} relation records
    commitments about the behaviour of the \emph{process}.  The standard
    application of these ideas is in the extension of 
    Hoare-like inference rules to quintuples that accommodate rely and guarantee conditions. 
    In contrast, in this paper, we embed rely-guarantee thinking
    into a refinement calculus for concurrent programs, in which programs are
    developed in (small) steps from an abstract specification.
    As is usual, we extend the implementation language with specification
    constructs (the extended language is sometimes called a wide-spectrum
    language), in this case adding (in addition to pre and postconditions) 
    two new commands:
    a guarantee command $(\mathbf{guar} g ~\cdot~ c)$ whose valid behaviours are in accord with the command $c$ 
    but all of whose atomic steps also satisfy the relation $g$,
    and 
    a rely command $(\mathbf{rely} r ~\cdot~ c)$ whose behaviours are like $c$ provided 
    any interference steps from the environment satisfy the relation $r$.
    The theory of concurrent program refinement is based on a 
    theory of atomic program steps and more
    powerful refinement laws, most notably, a law for decomposing a
    specification into a parallel composition, are developed from a small
    set of more primitive lemmas, which are proved sound with respect to an
    operational semantics.
  },
  month = sep,
  year = {2013}
}
@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}
}
@inproceedings{FPaNDEiITL,
  author = {Brijesh Dongol and John Derrick and Ian J. Hayes},
  title = {Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic},
  booktitle = {Proc.\ 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012)},
  conference = {Bamberg, Germany, 18-20 September 2012},
  editor = {Gerald L\"{u}ttgen and Stephan Merz},
  pages = {1--15},
  volume = {53},
  doi = {10.14279/tuj.eceasst.53.792},
  series = {Electronic Communications of the EASST},
  issn = {1863-2122},
  accepted = {Accepted 16 July 2012},
  published = {November 2012},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  abstract = {
   We propose Interval Temporal Logic as a basis for reasoning about concurrent programs with fine-grained atomicity due to the generality it provides over reasoning with standard pre/post-state relations. To simplify the semantics of parallel composition over intervals, we use fractional permissions, which allows one to ensure that conflicting reads and writes to a variable do not occur simultaneously. Using non-deterministic evaluators over intervals, we enable reasoning about the apparent states over an interval, which may differ from the actual states in the interval. The combination of Interval Temporal Logic, non-deterministic evaluators and fractional permissions results in a generic framework for reasoning about concurrent programs with fine-grained atomicity. We use our logic to develop rely/guarantee-style rules for decomposing a proof of a large system into proofs of its subcomponents, where fractional permissions are used to ensure that the behaviours of a program and its environment do not conflict.
  },
  keywords = {Interval Temporal Logic, Fractional Permissions, Non-deterministic 
    Expression Evaluation, Parallel Composition, Compositional Reasoning},
  year = {2012}
}
@inproceedings{TaAfRTP,
  author = {Brijesh Dongol and Ian J. Hayes and Larissa Meinicke and Kim Solin},
  affiliation = {School of Information Technology and Electrical Engineering, The University of Queensland, Australia},
  title = {Towards an Algebra for Real-Time Programs},
  booktitle = {13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS)},
  conference = {13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS), 17--20 September 2012, Cambridge, UK},
  accepted = {Accepted 12 July 2012},
  editor = {W. Kahl and T.G. Griffin},
  pages = {50--65},
  series = {LNCS},
  volume = {7560},
  isbn = {978-3-642-33313-2},
  issn = {0302-9743},
  publisher = {Springer},
  city = {Berlin / Heidelberg},
  doi = {10.1007/978-3-642-???-0_7},
  url = {http://dx.doi.org/10.1007/978-3-642-???-0_7},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  keywords = {Real-time, program algebra},
  abstract = {We develop an algebra for an interval-based model that has been shown to be useful for reasoning about real-time programs. In that model, a system's behaviour over all time is given by a stream (mapping each time to a state) and the behaviour over an interval is determined using an interval predicate, which maps an interval and a stream to a Boolean. Intervals are allowed to be open/closed at either end and adjoining (i.e., immediately adjacent) intervals do not share any common points but are contiguous over their boundary. Values of variables at the ends of open intervals are determined using limits, which allows the possible piecewise continuity of a variable at the boundaries of an interval to be handled in a natural manner. What sort of an algebra does this model give rise to? In this paper, we take a step towards answering that question by investigating an algebra of interval predicates.},
  year = {2012}
}
@inproceedings{DRTASCfMSS,
  author = {Brijesh Dongol and Ian J. Hayes},
  affiliation = {School of Information Technology and Electrical Engineering, The University of Queensland, Australia},
  title = {Deriving Real-time Action Systems Controllers from Multiscale System Specifications},
  booktitle = {Mathematics of Program Construction},
  conference = {11th International Conference on Mathematics of Program Construction (MPC), 25--27 June 2012, Madrid, Spain},
  accepted = {Accepted 19 March 2012},
  editor = {J. Gibbons and P. Nogueira},
  pages = {102--131},
  series = {LNCS},
  volume = {7342},
  isbn = {978-3-642-31112-3},
  issn = {0302-9743},
  publisher = {Springer},
  city = {Berlin / Heidelberg},
  doi = {10.1007/978-3-642-31113-0_7},
  url = {http://dx.doi.org/10.1007/978-3-642-31113-0_7},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  keywords = {Action systems},
  abstract = {This paper develops a method for deriving controllers for real-time systems in which the components of the system operate at different time granularities. To this end, we incorporate the theory of time bands into action systems, which allows one to structure a system into multiple abstractions of time. The framework includes a logic that facilitates reasoning about different types of sampling errors and transient properties (i.e., properties that only hold for a brief amount of time), and we develop theorems for simplifying proofs of hardware/software interaction. We formalise true concurrency and define refinement for the parallel composition of action systems. Our method of derivation builds on the verify-while-develop paradigm, where the action system code is developed side-by-side with its proof.},
  year = {2012}
}
@inproceedings{IOS,
  author = {Ian J. Hayes and Robert J. Colvin},
  affiliation = {School of Information Technology and Electrical Engineering, The University of Queensland, Australia},
  title = {Integrated Operational Semantics: Small-Step, Big-Step and Multi-Step},
  booktitle = {Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
  conference = {3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z, 18-21 June 2012, Pisa, Italy},
  accepted = {Invited keynote paper},
  editor = {Derrick, John and Fitzgerald, John and Gnesi, Stefania and Khurshid, Sarfraz and Leuschel, Michael and Reeves, Steve and Riccobene, Elvinia},
  pages = {21--35},
  series = {LNCS},
  volume = {7316},
  isbn = {978-3-642-30884-0},
  issn = {0302-9743},
  publisher = {Springer},
  doi = {10.1007/978-3-642-30885-7_2},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  abstract = {Plotkin's structural operational semantics provides a tried and tested method for defining the semantics of a programming language via sets of rules that define valid transitions between program configurations. Mosses' modular structural operational semantics (MSOS) recasts the approach by making use of rules consisting of labelled transitions, allowing a more modular approach to defining language semantics. MSOS can be adapted by using ``syntactic'' labels that allow local variables and aliasing to be defined without augmenting the semantics with environments and locations. The syntactic labels allow both state-based constructs of imperative languages and event-based constructs of process algebras to the specified in an integrated manner. To illustrate the integrated approach we compare its rules with Plotkin's original rules for both small-step and big-step operational semantics. One issue that arises is that defining concurrency requires the use of a small-step approach to handle interleaving, while defining a specification command requires a big-step approach. The integrated approach can be generalised to use a sequence of (small) steps as a label; we call this a multi-step operational semantics. This approach allows both concurrency and non-atomic specification commands to be defined.},
  year = {2012}
}
@inproceedings{RGRfTRPoMTB,
  author = {Brijesh Dongol and Ian J. Hayes},
  affiliation = {School of Information Technology and Electrical Engineering, The University of Queensland, Australia},
  title = {Rely/guarantee reasoning for teleo-reactive programs over multiple time bands},
  booktitle = {Integrated Formal Methods},
  conference = {9th International Conference on Integrated Formal Methods, 18-21 June 2012, Pisa, Italy},
  accepted = {Accepted 2 March 2012},
  editor = {Derrick, John and Gnesi, Stefania and Latella, Diego and Treharne, Helen},
  pages = {39--53},
  series = {LNCS},
  volume = {7321},
  isbn = {978-3-642-30728-7},
  issn = {0302-9743},
  publisher = {Springer},
  url = {http://dx.doi.org/10.1007/978-3-642-30729-4_4},
  doi = {10.1007/978-3-642-30729-4_4},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  keywords = {Teleo reactive},
  abstract = {A complex real-time system consists of components at multiple time abstractions with varying notions of granularity and precision. Existing hybrid frameworks only allow reasoning at a single granularity and at an absolute level of precision, which can be problematic because the models that are developed can become unimplementable. In this paper, we develop a framework that incorporates time bands so that the behaviour of each component may be specified at a time granularity that is appropriate for the component and its properties. We implement our controllers using teleo-reactive programs, which are high-level programs that are well-suited to controlling reactive systems in dynamic environments. We develop rely/guarantee-style reasoning rules and as an example, prove properties of a well-known mine-pump system.},
  year = {2012}
}
@incollection{MDWFVwUaO,
  tag = {springerlink:10.1007/978-3-642-27997-3_23},
  author = {Escott, Eban and Strooper, Paul and King, Paul and Hayes, Ian},
  affiliation = {School of Information Technology and Electrical Engineering, The University of Queensland, Brisbane, QLD 4072, Australia},
  title = {Model-Driven Web Form Validation with {UML} and {OCL}},
  booktitle = {Current Trends in Web Engineering},
  series = {Lecture Notes in Computer Science},
  editor = {Harth, Andreas and Koch, Nora},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {978-3-642-27996-6},
  keyword = {Computer Science},
  pages = {223-235},
  volume = {7059},
  url = {http://dx.doi.org/10.1007/978-3-642-27997-3\_23},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {LP0989363 BTLink},
  abstract = {Form validation is an integral part of a web application. Web developers must ensure that data input by the user is validated for correctness. Given the importance of form validation it must be considered as part of a model-driven solution to web development. Existing model-driven approaches typically have not addressed form validation as part of the model. In this paper, we present an approach that allows validation constraints to be captured within a model using UML and OCL. Our approach covers three common types of validation: single element, multiple element, and entity association. We provide an example to illustrate an architecture-centric approach.},
  year = {2012}
}
@inproceedings{AIRTSUTB,
  author = {B. Dongol and I. J. Hayes},
  title = {Approximating idealised real-time specifications using time bands},
  booktitle = {Automated Verification of Critical Systems 2011},
  editor = {A. Romanovsky and C. B. Jones and J. Bendiposto and M. Leuschel},
  pages = {1--16},
  volume = {46},
  doi = {10.14279/tuj.eceasst.46.684},
  series = {Electronic Communications of the EASST},
  issn = {1863-2122},
  publisher = {EASST},
  accepted = {Accepted 21 July 2011},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  abstract = {
    Timed specifications are often formalised at an absolute level of precision,
    which does not reflect the real world that the specifications model,
    i.e., in the real world, inputs cannot be sampled with absolute precision and
    physical hardware cannot react instantaneously.
    As a result the developed specifications can often become unimplementable.
    In this paper, we consider the time bands model
    which allows time to be structured into several layers of abstraction and
    relationships between bands to be formalised.
    This allows the timed specifications developed under idealised assumptions
    to be approximated using the time band in which the variables are sampled.
    We implement the approximated specifications using teleo-reactive programs
    embedded with time bands.
  },
  year = {2012}
}
@techreport{CMoNEE-TR,
  author = {I. J. Hayes and A. Burns and B. Dongol and C. B. Jones},
  title = {Comparing Models of Non\-deterministic Expression Evaluation},
  institution = {School of Computing Science, Newcastle University},
  pages = {1--21},
  number = {CS-TR-1273},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  keywords = {sampling logic},
  abstract = {
    Expression evaluation in programming languages is normally
    deterministic; however, if expressions involve variables that are
    being modified by the environment of the process during their
    evaluation, the result of the evaluation can be non\-deterministic.
    Two common cases where this occurs are in concurrent programs
    where processes share variables and real-time programs that
    interact to monitor and/or control their environment.
    In these contexts, while any particular evaluation of an expression
    gives a single result, there is a range of possible results that
    could be returned depending on the relative timing of modification
    of variables by the environment and their access within expression
    evaluation.
    Hence to model the semantics of expression evaluation one can use
    the set of possible values the expression evaluation could return.
    This paper considers three views of interpreting expressions
    nondeterministically.
    The paper formalises the three approaches,
    highlights different properties satisfied by the approaches,
    relates the approaches
    and
    explores conditions under which they coincide.
    Furthermore, a link is made to a new notation used in reasoning about interference.
  },
  month = {September},
  year = {2011}
}
@techreport{timebands-TR,
  author = {Alan Burns and Kun Wei and Jim Woodcock and Ian J. Hayes and Cliff B. Jones},
  title = {Timebands Framework -- 2011},
  number = {YCS-2011-467},
  pages = {1--36},
  note = {36 pages},
  institution = {Department of Computer Science, University of York},
  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, a timeband framework has been developed.
    In this paper we review this framework and report on modifications, extensions
    and applications that have been undertaken in funded research that completed in
    2011.},
  year = {2011}
}
@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}
}
@inproceedings{SEFM10,
  author = {K. Winter and I. J. Hayes and R. J. Colvin},
  title = {Integrating Requirements: The {Behavior Tree} Philosophy},
  booktitle = {Proc.\ of Int.\ Conf.\ on Software Engineering and Formal Methods (SEFM 2010)},
  editor = {J. L. Fiadeiro and S. Gnesi},
  accepted = {Accepted for publication 8 June 2010},
  pages = {41--50},
  publisher = {IEEE Computer Society Press},
  doi = {???},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {LP0989363 BTLink},
  keywords = {Requirements, modelling, analysis, integration, Behavior Tree},
  abstract = {Behavior Trees were invented by Geoff Dromey
    as a graphical modelling notation. Their design was driven
    by the desire to ease the task of capturing functional system
    requirements and to bridge the gap between an informal
    language description and a formal model. Vital to Dromey’s
    intention is the idea of incrementally building the model out
    of its building blocks, the functional requirements. This is
    done by graphically representing each requirement as its own
    Behavior Tree and incrementally merging the trees to form a
    more complete model of the system.
   
    In this paper we investigate the essence of this constructive
    approach to creating a model in general notation-independent
    terms and discuss its advantages and disadvantages. The result
    can be seen as a framework of rules and provides us with a
    semantic underpinning of requirements integration. Integration
    points are identified by examining the (implicit or explicit)
    preconditions of each requirement. We use Behavior Trees as
    an example of how this framework can be put into practise.
    },
  year = {2010}
}
@inproceedings{ICTAC10,
  author = {I. J. Hayes},
  title = {Invariants and Well-Foundedness in Program Algebra},
  booktitle = {International Colloquium on Theoretical Aspects of Computing (ICTAC)},
  fullbooktitle = {Theoretical Aspects of Computing – ICTAC 2010,
7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1-3, 2010. Proceedings},
  editor = {A. Cavalcanti and D. D\'{e}harbe and M.-C. Gaudel and J. Woodcock},
  pages = {1--14},
  series = {LNCS},
  volume = {6255},
  publisher = {Springer},
  city = {Berlin Heidelberg},
  doi = {10.1007/978-3-642-14808-8_1},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  keywords = {Program algebra},
  abstract = {Program algebras abstract the essential properties of programming
    languages in the form of algebraic laws.
    The proof of a refinement law may be expressed in terms of the
    algebraic properties of programs required for the law to hold, 
    rather than directly in terms of the semantics of a language.
    This has the advantage that the law is then valid for any programming
    language that satisfies the required algebraic properties.
    By characterised the important properties of programming languages
    algebraically we can devise simple proofs of common refinement laws. 
    In this paper we consider standard refinement laws for sequential programs.
    We give simple characterisations of program invariants and
    well foundedness of statements.},
  year = {2010}
}
@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}
}
@inproceedings{UTPtDNaA,
  author = {I. J. Hayes and S. E. Dunne and L. A. Meinicke},
  title = {Unifying Theories of Programming that Distinguish Nontermination and Abort},
  booktitle = {Mathematics of Program Construction},
  conference = {10th International Conference, MPC 2010, Qu\'{e}bec City, Canada, June 21-23, 2010, Proceedings},
  editor = {C. Bolduc and J. Desharnais and B. Ktari},
  pages = {178--194},
  series = {LNCS},
  volume = {6120},
  isbn = {978-3-642-13320-6},
  publisher = {Springer},
  city = {Berlin},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  keywords = {Unifying theories of programming},
  abstract = {In this paper we focus on the relationship between a number of
    specification models. The models are formulated in the Unifying Theories of
    Programming of Hoare and He, but correspond to widely used specification models.
    We cover issues such as partial correctness, total correctness, and general correctness.
    The properties we use to distinguish the models are these:
      whether they allow the specification of assumptions about the initial state
      outside of which no guarantees are given about the behaviour of the program,
      i.e., the program may "abort";
      whether a specification may allow or even require nontermination as a valid
      (non-aborting) outcome; and
      whether they allow the expression of tests or enabling conditions, outside of
      which the program has no possible behaviour.
    When considering termination, we consider both an abstract model, which only
    distinguishes whether a program terminates or not, as well as models that include
    a notion of time: either abstract time representing a notion of progress or real-time.},
  year = {2010}
}
@inproceedings{CASDUEP,
  author = {Brijesh Dongol and Ian J. Hayes},
  title = {Compositional Action System Derivation Using Enforced Properties},
  booktitle = {Mathematics of Program Construction (MPC)},
  conference = {10th International Conference, MPC 2010, Qu\'{e}bec City, Canada, June 21-23, 2010, Proceedings},
  accepted = {Accepted for publication 21 Feb 2010},
  editor = {C. Bolduc and J. Desharnais and B. Ktari},
  pages = {119--139},
  series = {LNCS},
  volume = {6120},
  issn = {0302-9743},
  publisher = {Springer Verlag},
  city = {Berlin},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  keywords = {Action systems},
  abstract = {Action systems have been shown to be applicable for modelling and
    constructing both sequential and concurrent systems.
    This paper presents an approach to program construction
    where the concrete implementation is derived from its specification---via a
    series of small refinements---using incomplete proofs to motivate changes to
    the program.
    Formalisation of our approach is provided by enforced properties,
    which restrict the traces of a program to those that satisfy the enforced
    properties.
    The goal of the derivation is to refine a program with enforced properties
    to a program (with no enforced properties) whose code satisfies the enforced
    properties.
    An advantage of this approach is that the code in the earlier versions of the
    program need not be complete; incorrect execution of the program is avoided
    by including enforced properties in the specification.
    Enforced properties may be any temporal formula or relation, and hence we may
    reason about both safety and progress in a compositional setting.},
  year = {2010}
}
@inproceedings{UTP08,
  author = {Steve E. Dunne and Ian J. Hayes and Andy J. Galloway},
  title = {Reasoning about Loops in Total and General Correctness},
  booktitle = {Unifying Theories of Programming: Second International Symposium, UTP 2008, Dublin, Ireland, September 8-10, 2008, Revised Selected},
  shortbooktitle = {Unifying Theories of Programming (UTP 2008)},
  editor = {A. Butterfield},
  volume = {5713},
  series = {Lecture Notes in Computer Science},
  pages = {62--81},
  publisher = {Springer},
  city = {Berlin Heidelberg},
  isbn = {978-3-642-14520-9},
  issn = {0302-9743},
  doi = {10.1007/978-3-642-14521-6_5},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR/DP0558408 FTRT},
  abstract = {We introduce a calculus for reasoning about programs in total correctness
    which blends UTP designs
    with von Wright's notion of a demonic refinement algebra.
    We demonstrate its utility in verifying
    the familiar loop-invariant  rule for refining
    a total-correctness specification by a while loop.
    Total correctness equates non-termination with completely
    chaotic behaviour, with the consequence that any situation which
    admits non-termination must also admit arbitrary
    terminating behaviour. General correctness
    is more discriminating in allowing non-termination to be
    specified together with more particular terminating behaviour.
    We therefore introduce an analogous calculus for reasoning about
    programs in general correctness which blends UTP prescriptions with
    a demonic refinement algebra.
    We formulate a loop-invariant rule for refining
    a general-correctness specification by a while loop,
    and we use our general-correctness calculus to verify
    the new rule.},
  year = {2010}
}
@inproceedings{ASWEC09,
  author = {Brijesh Dongol and Ian J. Hayes},
  title = {Enforcing Safety and Progress Properties:
            An Approach to Concurrent Program Derivation},
  booktitle = {Australian Software Engineering Conference},
  conference = {20th Australian Software Engineering Conference (ASWEC 2009),
               14-17 April 2009, Gold Cost, Australia},
  editor = {Colin Fidge},
  pages = {3--12},
  publisher = {IEEE Computer Society},
  isbn = {978-0-7695-3599-9},
  ee = {http://dx.doi.org/10.1109/ASWEC.2009.12},
  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 = {DP0987452 TFTR-FTRT/CEO348249 ACCS},
  abstract = {In this paper we develop an approach for deriving concurrent
    programs.  At any stage in its derivation, a program consists of a
    combination of the code for its processes together with a set of
    \emph{enforced} properties.  The behaviour of such a combination
    consists of those behaviours of the code that satisfy the enforced
    properties. Because enforced properties are temporal formulae, they
    may be used to enforce both safety and progress properties of the
    program. While the code by itself is executable, when combined with
    enforced properties, the program is not yet in an executable form. A
    derivation starts from a program in which the desired properties of
    the code are expressed via enforced properties, and the goal is to
    derive a program with additional code but no enforced properties. We
    outline a trace-based theory which formalises the meaning of
    programs with enforced properties, and transformation rules that
    ensure each modified program is a refinement of the original.},
  year = {2009}
}
@inproceedings{IFM09,
  author = {R. J. Colvin and I. J. Hayes},
  title = {{CSP} with Hierarchical State},
  booktitle = {Integrated Formal Methods (IFM 2009)},
  editor = {M. Leuschel and H. Wehrheim},
  publisher = {Springer},
  series = {LNCS},
  volume = {5423},
  pages = {118--135},
  issn = {0302-9743},
  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},
  abstract = {The process algebra CSP is designed for specifying interactions between
    concurrent systems.  In CSP, and related languages, concurrent processes
    synchronise on common events, while the internal operations of the
    individual processes are treated abstractly.  In some contexts, however,
    such as when modelling systems of systems, it is desirable to model both
    interprocess communications as well as the internal operations of
    individual processes.  At the implementation level, shared state is
    often the method of communication between processes, and tests and
    updates of local state are used to implement internal operations.  In
    this paper we propose an extension of the CSP language which maintains
    CSP's core elegance in specifying process synchronisation, while also
    allowing state-based behaviour.  State is treated \emph{hierarchically},
    allowing (nested) declarations of local and shared variables.  The state
    can be accessed and modified using a refinement calculus-style
    \emph{specification command}, which may be optionally paired with  event
    synchronisation.  The semantics of the extended language, preserves the
    original CSP rules.  The approach we present is novel in that state is
    part of the process, rather than a meta-level construct appearing only
    in the rules.},
  year = {2009}
}
@incollection{DDFvIC,
  author = {Ian J. Hayes},
  title = {Dynamically Detecting Faults via Integrity Constraints},
  booktitle = {Methods, Models, and Tools for Fault Tolerance},
  editor = {Michael Butler and Cliff Jones and Alexander Romanovsky and Elena Troubitsyna},
  volume = {5454},
  publisher = {Springer Verlag},
  isbn = {978-3-642-00866-5},
  issn = {0302-9743},
  series = {Lecture Notes in Computer Science},
  pages = {85--103},
  abstract = {Control programs for safety-critical systems are required
    to tolerate
    faults in the devices they control.
    In this paper we examine a systematic approach to devising code to
    detect faulty devices at runtime.
    The approach is centred around the
    use of integrity constraints,
    which are invariants on the state of a
    system's variables, including its inputs and outputs.
    Under normal operation integrity constraints should always hold,
    but they are designed to fail to hold if there is a fault.
    By adding variables to capture
    the previous state of variables or
    the time of significant events,
    additional integrity constraints can be devised to check for
    faults in state transitions or
    faults with the rate of progress of the system.
    We discuss techniques for devising integrity constraints as well as
    efficiently evaluating the constraints.
    When an error is detected via the failure of an integrity constraint,
    the integrity constraint(s) that failed can help diagnose the
    likely fault.
    We illustrate the approach using controller software written in the
    action system style,
    but it is equally applicable to other state machine approaches such as
    Event-B and TLA.},
  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 = {DP0987452 TFTR/DP0558408 FTRT},
  year = {2009}
}
@inproceedings{serene08,
  author = {Ian J. Hayes},
  title = {Towards reasoning about teleo-reactive programs for robust real-time systems},
  booktitle = {Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems},
  editor = {Nicolas Guelfi and Henry Muccini and Patrizio Pelliccione and Alexander Romanovsky},
  isbn = {978-1-60558-275-7},
  pages = {87--94},
  conference = {17--19 Nov 2008, Newcastle upon Tyne, United Kingdom},
  organisation = {European Research Consortium for Informatics and Mathematics and ACM SIGSOFT},
  doi = {http://doi.acm.org/11.1145/1479772.1479789},
  publisher = {ACM},
  address = {New York, NY, USA},
  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 = {The teleo-reactive programming approach was developed by Nilsson for
    application in domains like robotics.
    It has a high-level programming model that allows real-time
    control programs to be written in a manner that allows them to
    react robustly to changes in the environment.
    In this paper we give a formalisation of the semantics of
    teleo-reactive programs and provide rely/guarantee rules for
    reasoning about them.
    The semantics are given in a form
    that partitions the behaviour of the system into
    its behaviour over a sequence of time intervals.},
  year = {2008}
}
@inproceedings{PCiRA,
  author = {Larissa Meinicke and Ian J. Hayes},
  title = {Probabilistic Choice in Refinement Algebra},
  booktitle = {Mathematics of Program Construction (MPC)},
  editor = {Philippe Audebaud and Christine Paulin-Mohring},
  pages = {243--267},
  series = {Lecture Notes in Computer Science},
  volume = {5133},
  publisher = {Springer Verlag},
  doi = {10.1007/978-3-540-70594-9_14},
  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},
  keywords = {Kleene algebra, probability, refinement algebra, total-correctness},
  abstract = {The term refinement algebra refers to a set of abstract algebra,
    similar to Kleene algebra with tests, that are suitable for reasoning 
    about programs in a total-correctness framework. 
    Abstract algebraic reasoning also works well when probabilistic programs 
    are concerned, and a refinement algebra that is suitable for such 
    programs has been defined. 
    This refinement algebra does not contain a probabilistic choice operator, 
    and has been used to define commonalities between a variety of 
    different -- both probabilistic and non-probabilistic -- program models. 
    Although it is possible to algebraically verify a large and interesting 
    group of theorems for probabilistic programs without explicit reference 
    to probabilistic choices, there are circumstances in which reasoning 
    directly about probabilistic choices may be useful. 
    In this paper we investigate how probabilistic choice may be 
    characterised abstract-algebraically in refinement algebra. 
    That is, we propose a new refinement algebra in which probabilistic 
    choice, probabilistic guards and assertions may be expressed. 
    Two operators for modelling probabilistic enabledness and termination 
    are also introduced.},
  year = {2008}
}
@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}
}
@techreport{TSftOGTIwtPLfU07-TR,
  author = {Brijesh Dongol and Ian J. Hayes},
  title = {Trace Semantics for the {Owicki-Gries} Theory Integrated with the Progress Logic from UNITY},
  number = {SSE-2007-02},
  institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
  year = {2007}
}
@inproceedings{JHJ07,
  author = {C. B. Jones and I. J. Hayes and M. A. Jackson},
  booktitle = {Formal Methods and Hybrid Real-Time Systems},
  date-modified = {2007-10-18 15:45:50 +0100},
  editor = {C. B. Jones and Z. Liu and J. Woodcock},
  pages = {364--390},
  publisher = {Springer Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Deriving Specifications for Systems That are Connected to the Physical World},
  volume = {4700},
  ibsn = {978-3-540-75220-2},
  doi = {10.1007/978-3-540-75221-9},
  project = {CEO348249 ACCS},
  abstract = {Well understood methods exist for developing programs from formal
      specifications.
      Not only do such methods offer a precise check that certain sorts of deviations
      from their specifications are absent from implementations
      but they can also increase the productivity of the development process by
      careful use of layers of abstraction and refinement in design.
      These methods, however, presuppose a
      specification from which to begin the development.
      For tasks that are fully described in terms of the symbolic values
      within a machine, inventing a specification is not difficult
      but there is an
      increasing demand for systems in which programs interact with an
      external physical world.
      Here, the task of fixing the specification for the ``silicon package''
      can be more challenging than the development itself.
      Such applications include control programs that attempt to bring
      about changes in the physical world via actuators and measure things
      in that external (to the silicon package) world via sensors.
      Furthermore, most systems of this class must tolerate failures in the
      physical components outside the computer:
      it then becomes even harder
      to achieve confidence that the specification is appropriate.
      This paper offers a systematic way to {\em derive\/} the specification of
      a control program.
      Furthermore, our approach leads to recording
      assumptions about the physical world.
      We also discuss separating the detection and
      management of faults from system operation in the absence of faults.
      This discussion is linked to the distinction between
      ``normal'' and ``radical'' design.},
  year = 2007
}
@techreport{ASfBT-TR,
  author = {R. Colvin and I.J. Hayes},
  title = {A Semantics for Behavior Trees},
  institution = {ARC Centre for Complex Systems (ACCS)},
  type = {ACCS Technical Report},
  number = {ACCS-TR-07-01},
  url = {http://www.accs.edu.au/documents/TechnicalReports/ACCS_TR_07_01},
  month = {April},
  project = {CEO348249 ACCS},
  year = {2007}
}
@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
}
@inproceedings{RAaPL-ICFEM06,
  author = {L. Meinicke and I. J. Hayes},
  title = {Reasoning Algebraically about Probabilistic Loops},
  booktitle = {ICFEM},
  editor = {Zhiming Liu and Jifeng He},
  series = {LNCS},
  volume = {4260},
  publisher = {Springer Verlag},
  city = {Berlin},
  isbn = {3-540-47460-9},
  issn = {0302-9743},
  pages = {380--399},
  conference = {1--3 November 2006, Macau, PRC},
  doi = {10.1007/11901433_21},
  url = {http://dx.doi.org/10.1007/11901433\_21},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {DP0558408 FTRT},
  year = {2006},
  abstract = {
    Back and von Wright have developed algebraic laws for reasoning
    about loops in 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. In particular we focus on developing
    data refinement rules for probabilistic action systems. 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. In particular, our probabilistic action system data
    refinement rules are new.}
}
@inproceedings{CASR-MPC06,
  author = {Larissa Meinicke and Ian J. Hayes},
  title = {Continuous Action System Refinement},
  booktitle = {Mathematics of Program Construction: Proceedings 8th International Conference (MPC 2006)},
  editor = {T. Uustalu},
  series = {LNCS},
  volume = {4014},
  publisher = {Springer Verlag},
  city = {Berlin},
  isbn = {3-540-35631-2},
  issn = {0302-9743},
  pages = {316--337},
  conference = {3--5 July 2006, Kuressaare, Estonia},
  doi = {10.1007/11783596_19},
  url = {http://dx.doi.org/10.1007/11783596_19},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {DP0558408 FTRT},
  year = {2006},
  abstract = {
    Action systems are a framework for reasoning about discrete
    reactive systems. Back, Petre and Porres have extended these action sys-
    tems to continuous action systems, which can be used to model hybrid
    systems. In this paper we define a refinement relation, and develop prac-
    tical refinement rules for continuous action systems.
    The meaning of continuous action systems is expressed in terms of a
    mapping from continuous action systems to action systems. First, we
    present a new mapping from continuous action systems to action systems,
    such that the definition of trace refinement is correct with respect to it.
    Second, we present a stream semantics that is compatible with the trace
    semantics, but is preferable to it because it is more general. Although
    action system trace refinement rules are applicable to continuous action
    systems with a stream semantics, they are not complete. Finally, we
    introduce a new data refinement rule that is valid with respect to the
    stream semantics and can be used to prove refinements that are not
    possible in the trace semantics, and we analyse the completeness of our
    new rule in conjunction with the existing trace refinement rules.}
}
@inproceedings{UTP06,
  author = {I. J. Hayes},
  title = {Termination of real-time programs: definitely, definitely not or maybe},
  booktitle = {UTP 2006: First Int.\ Symp.\ on Unifying Theories of Programming},
  editor = {S. E. Dunne and W. J. Stoddart},
  series = {LNCS},
  volume = {4010},
  isbn = {3-540-34750-X},
  issn = {0302-9743},
  publisher = {Springer},
  pages = {141--154},
  conference = {6--7 Feb 2006, Darlington, UK},
  acceptance = {Invited keynote paper},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {DP0558408 FTRT},
  year = {2006},
  abstract = {Real-time control programs are often used in contexts where
    (conceptually)
    they run forever.
    Repetitions within such programs (or their specifications) may either
    (i) be guaranteed to terminate,
    (ii) be guaranteed to never terminate (loop forever),
    or
    (iii) may possibly terminate.
    In dealing with real-time programs and their specifications,
    we need to be able to represent these possibilities,
    and define suitable refinement orderings.

    A refinement ordering based on Dijkstra's weakest precondition only
    copes with the first alternative.
    Weakest liberal preconditions allow
    one to constrain behaviour provided the program terminates,
    which copes with the third alternative to some extent.
    However, neither of these handles the case when a program does not 
    terminate.
    To handle this case a refinement ordering based on relational  
    semantics can be used.
    In this paper we explore these issues 
    and 
    the definition of loops for real-time programs
    as well as corresponding refinement laws.}
}
@techreport{BurnsEt05,
  author = {A. Burns and I. J. Hayes and G. Baxter and C. J. Fidge},
  title = {Modelling Temporal Behaviour in Complex Socio-Technical Systems},
  year = {2005},
  institution = {University of York},
  url = {https://www.cs.york.ac.uk/rts/publications/Burns2005.html},
  pdf = {../Papers/R_Burns_2005.pdf},
  number = {YCS~390}
}
@proceedings{FM05,
  editor = {J. Fitzgerald and I.J. Hayes and A. Tarlecki},
  title = {FM 2005: Formal Methods -- Proceedings
    13th International Symposium of Formal Methods Europe,
    Newcastle, UK, July 2005},
  ibsn = {3-540-27882-6},
  issn = {0302-9743},
  volume = {3582},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  city = {Berlin},
  month = {July},
  conference = {Newcastle, UK, 18--22 July 2005},
  project = {CEO348249 ACCS},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  year = {2005}
}
@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}
}
@inproceedings{IoGPATiaSDE,
  author = {Erica Glynn and I.J. Hayes and Anthony MacDonald},
  title = {Integration of generic program analysis tools into a software development environment},
  booktitle = {Computer Science 2005:
    Proceedings 28th Australasian Computer Science Conference (ACSC2005)},
  volume = {38},
  publisher = {Australian Computer Society},
  isbn = {1-920682-20-1},
  issn = {1445-1336},
  series = {Conferences in Research and Practice in Information Technology},
  editor = {V. Estivill-Castro},
  pages = {249--257},
  conference = {31 Jan--3 Feb 2005, Newcastle},
  acceptance = {41/122 for full papers},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {DP0209722 CRTR/CEO348249 ACCS/Erica Honours},
  year = {2005},
  abstract = {
    Support for program understanding in development and maintenance tasks
    can be facilitated by program analysis techniques.
    Both control-flow and data-flow analysis can support program
    comprehension by augmenting the program text with additional
    information that may either be displayed with the program or
    used to allow more sophisticated navigation of the program,
    e.g., from an identifier's use to its definition.

    This paper outlines the addition of generic program analysis
    support to a generic, language-based, software development environment.
    The analysis tools are implemented in two phases:
    a language-dependent phase that extracts basic information from
    the program, such as its control-flow graph;
    and
    a language-independent phase that performs a more sophisticated
    analysis of the basic information.
    This separation allows program analysis tools to be easily generated
    for a new language.}
}
@techreport{BaFICBE05,
  author = {Cook, Phil and Welsh, Jim and Hayes, Ian J.},
  title = {Building a Flexible Incremental Compiler Back-End},
  number = {SSE-2005-02},
  institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
  year = {2005}
}
@techreport{ISEfIS05,
  author = {Cook, Phil and Welsh, Jim and Hayes, Ian J.},
  title = {Incremental Semantic Evaluation for Interactive Systems: Inertia, Pre-emption, and Relations},
  number = {SSE-2005-01},
  institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
  year = {2005}
}
@inproceedings{AEfBaSOoiR,
  author = {C. Smith and K. Winter and I. J. Hayes and R. G. Dromey and P. A. Lindsay and D. A. Carrington},
  title = {An environment for building a system out of its requirements},
  booktitle = {Proc.\ 19th IEEE Int.\ Conf.\ on Automated Software Engineering},
  publisher = {IEEE},
  pages = {398--399},
  conference = {??},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {CEO348249 ACCS/DCCS},
  year = {2004}
}
@incollection{DLPfSUSR,
  author = {R. Colvin and L. Groves and I.J. Hayes and D. Hemer and R. Nickson and P.A. Strooper},
  title = {Developing Logic Programs from Specifications Using Stepwise Refinement},
  booktitle = {Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development},
  series = {Lecture Notes in Computer Science},
  volume = {3049},
  editor = {Bruynooghe, Maurice and Lau, Kung-Kiu},
  isbn = {3-540-22152-2},
  issn = {0302-9743},
  publisher = {Springer Verlag},
  city = {Berlin},
  pages = {66--89},
  totalchap = {15},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {A49937007 RefLP},
  year = {2004},
  abstract = {In this paper we demonstrate a refinement calculus for logic
    programs, which is a framework for developing logic programs from
    specifications.
    The paper is written in a tutorial-style, using a running example to
    illustrate how the refinement calculus is used to develop logic programs.
    The paper also presents an overview of some of the advanced features of
    the calculus,
    including the introduction of higher-order procedures and the refinement
    of abstract data types.}
}
@inproceedings{TPIRTS,
  author = {I. J. Hayes},
  title = {Towards Platform-Independent Real-Time Systems},
  booktitle = {ASWEC},
  editor = {P. A. Strooper},
  publisher = {IEEE Computer Society},
  city = {Los Alamitos, California},
  pages = {192--200},
  conference = {13-16 April 2004, Melbourne},
  acceptance = {36/79 for full papers},
  isbn = {0-7695-2089-8},
  issn = {1530-0803},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {DP0209722 CRTR},
  year = {2004},
  abstract = {
    Real-time software systems are rarely developed once and left to run. 
    They are subject to changes of requirements as the applications
    they support expand, and they commonly outlive the platforms
    they were designed to run on. 
    A successful real-time system will be duplicated and 
    adapted to a variety of applications---it becomes a product line.
    Current methods for real-time software development are commonly based
    on low-level programming languages and involve considerable
    duplication of effort when a similar system is to be developed or the
    hardware platform changes.

    To provide more dependable, flexible and maintainable real-time
    systems at a lower cost what is needed is a platform-independent
    approach to real-time systems development.
    The development process is composed of two phases:
    a platform-independent phase, that defines the desired system
    behaviour and develops a platform-independent design and
    implementation,
    and
    a platform-dependent phase that maps the implementation onto the
    target platform.
    The last phase should be highly automated.
    For critical systems, assessing dependability is crucial.
    The partitioning into platform dependent and independent phases has to
    support verification of system properties through both phases.}
}
@inproceedings{PaP,
  author = {I.J. Hayes},
  title = {Programs as paths: An approach to timing constraint analysis},
  booktitle = {ICFEM},
  editor = {Jin Song Dong and Jim Woodcock},
  publisher = {Springer Verlag},
  city = {Berlin},
  series = {LNCS},
  volume = {2885},
  pages = {1--15},
  conference = {5--7 November 2003, Singapore},
  acceptance = {34/91 for full papers},
  isbn = {3-540-20461-X},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {DP0209722 CRTR},
  year = {2003},
  abstract = {A program can be decomposed into a set of possible execution
    paths.
    These can be described in terms of primitives such as
    assignments, assumptions and coercions,
    and composition operators such as
    sequential composition and nondeterministic choice
    as well as finitely or infinitely iterated sequential composition.
    Some of these paths cannot possibly be followed
    (they are dead or infeasible),
    and they may or may not terminate.

    Decomposing programs into paths provides a foundation for
    analyzing properties of programs.
    Our motivation is timing constraint analysis of real-time programs,
    but the same techniques can be applied in other areas such as
    program testing.
    In general the set of execution paths for a program is infinite.
    For timing analysis we would like to decompose a program into a finite
    set of subpaths that covers all possible execution paths,
    in the sense that we only have to analyze the subpaths in
    order to determine suitable timing constraints that cover all
    execution paths.}
}
@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.}
}
@inproceedings{DtSoaCSftoiE,
  author = {I.J. Hayes and M.A. Jackson and C.B. Jones},
  title = {Determining the Specification of a Control System from that of its Environment},
  booktitle = {{FME 2003}: Formal Methods},
  editor = {K. Araki and S. Gnesi and D. Mandrioli},
  publisher = {Springer Verlag},
  city = {Berlin},
  series = {LNCS},
  volume = {2805},
  pages = {154--169},
  pdf = {../Papers/fme03.pdf},
  conference = {10-12 September 2003, Pisa, Italy},
  acceptance = {44/144 for full papers},
  isbn = {3-540-40828-2},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {CEO348249 ACCS/DCCS},
  year = {2003},
  abstract = {Well understood methods exist for developing
    programs from given specifications. A formal
    method identifies proof obligations at each
    development step: if all such proof obligations
    are discharged, a precisely defined class of
    errors can be excluded from the final program.
    For a class of ``closed'' systems such methods
    offer a gold standard against which less formal
    approaches can be measured.

    For ``open'' systems --those
    which interact with the physical world-- the
    task of obtaining the program specification can
    be as challenging as the task of deriving the
    program. And, when a system of this class must
    tolerate certain kinds of unreliability in the
    physical world, it is still more challenging to
    reach confidence that the specification obtained
    is adequate. We argue that widening the notion
    of software development to include specifying
    the behaviour of the relevant parts of the
    physical world gives a way to derive the
    specification of a control system and also to
    record precisely the assumptions being made
    about the world outside the computer.}
}
@inproceedings{lp-ho,
  author = {R. Colvin and I. J. Hayes and D. Hemer and P.A. Strooper},
  title = {Refinement of higher-order logic programs},
  booktitle = {{Proceedings of the International Workshop on
            Logic-based Program Synthesis and Transformation (LOPSTR 2002)}},
  editor = {M. Leuschel},
  publisher = {Springer},
  city = {Berlin},
  series = {Lecture Notes in Computer Science},
  volume = {2664},
  pages = {126--143},
  acceptance = {15/40 for full papers},
  project = {A49937007 RefLP},
  year = {2003},
  abstract = {A refinement calculus provides a method for transforming
   specifications to executable code, maintaining the correctness of
   the code with respect to its specification. In this paper we extend
   the refinement calculus for logic programs to include higher-order
   programming capabilities in specifications and programs, such as
   procedures as terms and lambda abstraction. We use a higher-order type
   and term system to describe programs, and provide a semantics for the
   higher-order language and refinement. The calculus is illustrated by
   refinement examples.}
}
@inproceedings{RaDiCRTP,
  author = {Sibylle Peuker and Ian Hayes},
  title = {Reasoning about Deadlines in Concurrent Real-Time Programs},
  booktitle = {Workshop on Formal Methods for Parallel Programming (FMPP 2003)  in Proc.\ 17th International Parallel and Distributed Processing Symposium},
  editor = {Michel Charpentier and Beverly Sanders},
  publisher = {IEEE CS Press},
  pages = {1-8},
  isbn = {0-7695-1926-1},
  conference = {Workshop on Formal Methods for Parallel Programming (FMPP 2003)},
  url = {http://www.cs.unh.edu/~charpov/FMPPTA/},
  svrctr = {02--37},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {DP0209722 CRTR},
  year = {2003},
  abstract = {We propose a method for the timing analysis of concurrent
    real-time programs with hard deadlines. We divide the analy\-sis into
    a machine-independent and a machine-dependent task.   The latter takes
    into account the execution times of the program on a particular
    machine. Therefore, our goal is to make the machine-dependent phase of
    the analysis as simple as possible.

    We succeed in the sense that the machine-dependent phase remains the
    same as in the analysis of sequential programs. We shift the
    complexity introduced by concurrency completely to the
    machine-in\-de\-pen\-dent phase.}
}
@inproceedings{FSfPP,
  author = {K. Lermer and C. J. Fidge and I. J. Hayes},
  title = {Formal Semantics for Program Paths},
  booktitle = {Computing: The Australian Theory Symposium (CATS) 2003},
  editor = {J. Harland},
  publisher = {Elsevier},
  series = {Electronic Notes in Theoretical Computer Science (ENTCS)},
  volume = {78},
  pages = {1--24},
  isbn = {0444510850},
  conference = {4--7 February, 2003, Adelaide, Australia},
  month = feb,
  url = {http://www.elsevier.nl/locate/entcs/volume78.html},
  svrctr = {SVRC-TR-02-05},
  project = {DP0209722 CRTR/A49937045 TPA},
  year = {2003},
  abstract = {This paper provides the syntax and semantics for a
    systematic approach
    to the problem of analysing
    control-flow paths in computer programs.
    We give an abstract syntax and a partial
    correctness semantics
    for program control-flow paths
    as a generic model for path analysis
    and constraint derivation.
    This approach is formally based on a predicate transformer
    semantics over
    a boolean-valued predicate space and an
    abstract command language.
    The notions of a command,
    dead commands, the entry and exit
    conditions of a command and the inverse of a command
    are formally defined and investigated on the base of the
    semantics. A notion of command refinement
    is introduced capturing the abstraction
    process in program development
    from specification to implementation with
    partial correctness.
    Furthermore, command-reduction theorems and
    characterisations for command refinement are
    derived using the underlying semantics.
    Finally we verify the equivalence
    of weakest liberal precondition and strongest
    postcondition semantics for program commands in terms
    of the ordering relation they define on the command language.
    The approach is generic in that it is
    applicable to any program language that can be
    supplied with a predicate transformer semantics.},
  keywords = {Control-flow path analysis; Partial correctness semantics;
    Path refinement;
    Weakest liberal precondition semantics; Strongest postconditions.}
}
@incollection{APSfRTR,
  author = {I. J. Hayes},
  title = {A Predicative Semantics for Real-Time Refinement},
  booktitle = {Programming Methodology},
  editor = {A. McIver and C. C. Morgan},
  publisher = {Springer},
  city = {New York},
  pages = {109--133},
  isbn = {0-387-95349-3},
  totalchap = {20},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  svrctr = {01-15},
  project = {DP0209722 CRTR/A49801500 HertZ},
  year = {2003},
  abstract = {Real-time systems play an important role in many safety-critical
    systems.
    Hence it is essential to have a formal basis for the
    development of real-time software.
    In this chapter we present a predicative semantics
    for a real-time language.
    The semantics includes a special variable representing the current time,
    and uses timed traces to present the values of external input and
    outputs over time so that reactive control systems can be handled.
    Because a real-time control system may be a nonterminating process,
    we allow the specification of nonterminating programs and the
    development of nonterminating repetitions. }
}
@techreport{ICSEiC-TR,
  author = {Phil Cook and Jim Welsh and Ian J. Hayes},
  title = {Incremental Context-Sensitive Evaluation in Context},
  institution = {Software Verification Research Centre, The University of
    Queensland},
  number = {02-11},
  project = {Phil PhD},
  year = {2002}
}
@inproceedings{lp-ho-EXTABS,
  author = {R. Colvin and I. J. Hayes and D. Hemer and P.  Strooper},
  title = {Extended abstract: Refinement of higher-order logic programs},
  booktitle = {{Pre-Proceedings of the International Workshop on
            Logic-based Program Synthesis and Transformation (LOPSTR 2002)}},
  editor = {M. Leuschel and F. Bueno},
  publisher = {School of Computer Science, Technical University of Madrid},
  pages = {136--141},
  conference = {17-20 September 2002, Technical University of Madrid},
  note = {Extended abstract},
  project = {A49937007 RefLP},
  year = {2002}
}
@techreport{BSAG-TR,
  author = {Ian J. Hayes},
  title = {Block-Structured (Attribute) Grammars},
  institution = {Software Verification Research Centre, The University of Queensland},
  number = {02-47},
  month = dec,
  project = {},
  code = {K (Research report)},
  rfcd = {280303 (Programming Languages)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  year = {2002},
  abstract = {
    Most computing languages are highly structured but
    conventional (flat) grammars
    do not make that structure explicit.
    To address this issue, we examine adding block structure
    to grammars.
    We allow a production in a grammar to have local productions
    associated with it.
    The local productions are accessible only via that production.
    Local productions for one construct may be nested within
    local productions for higher level constructs to form a
    tree-structured hierarchy.

    If block structuring is used with an attribute grammar one
    can also avoid explicit copying of inherited attributes
    through intermediate nodes in the parse tree that do not
    modify or make use of the attribute.
    For example, in the definition of an expression in a
    programming language grammar one may have an environment
    attribute that is identical for all nodes in the expression
    subtree.
    The explicit passing down of the environment attribute
    through the intermediate nodes
    can be avoided by allowing direct reference to the
    environment attribute of the top-level expression
    nonterminal.
  },
  keywords = {Block structure; attribute grammars; L-attribute grammars; 
    upward remote attributes.}
}
@inproceedings{ROOIaDC,
  author = {Jamie Shield and Ian J. Hayes},
  title = {Refining Object-Oriented Invariants and Dynamic Constraints},
  rfcd = {280303 (Programming Languages)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  pages = {52--61},
  doi = {10.1109/APSEC.2002.1182975},
  booktitle = {Asian-Pacific Software Engineering Conference (APSEC)},
  isbn = {0-7695-1850-8},
  editor = {P.A. Strooper and P. Muenchaisri},
  conference = {Ninth APSEC, 4--6 December 2002, Gold Coast, Queensland, Australia},
  issn = {1530-1362},
  publisher = {IEEE Computer Society},
  svrctr = {02-25},
  classification = {E},
  project = {Jamie PhD},
  convenor = {Australian Computer Society},
  url = {http://computer.org},
  year = {2002},
  abstract = {An invariant is a constraint on a class
    which holds for each externally accessible state of its
    instances.  A dynamic constraint is a dual-state
    property dictating before to after state behaviour that
    all methods must adhere to.  Both invariants and
    dynamic constraints are of practical benefit as they
    allow explicit declaration of high-level behavioural
    constraints on a class and all its sub-classes.  In
    this paper, formalisations of invariants and dynamic
    constraints are provided in the refinement calculus.
    Each is separated into coerced (specification) and
    extant (implemented or documentation) categories.
    Refinement rules are provided for strengthening
    invariants and dynamic constraints.  Two separate
    development paths are identified: (behavioural)
    sub-classing and private refinement.
    Refining a class may violate its invariant or dynamic
    constraint.  Sub-classing is a constrained form of
    refinement that maintains these properties.
    Revised refinement laws are provided.
    Private refinement is an alternative to
    (behavioural) sub-classing. It also maintains
    properties such as invariants and dynamics constraints
    and foregoes the constraints of sub-classing.  The
    disadvantage is that private refinement can only be
    used to implement a class.},
  keywords = {Object-Oriented, Refinement Calculus, Invariants, 
    History Properties}
}
@inproceedings{TaRCfCRTP,
  author = {S. Peuker and I.J. Hayes},
  title = {Towards a Refinement Calculus for Concurrent Real-Time Programs},
  editor = {C. George and Huaikou Miao},
  booktitle = {Formal Methods and Software Engineering (ICFEM)},
  conference = {Proceedings 4th Int. Conf. on Formal Engineering Methods
    (ICFEM 2002), Shanghai, China, October 2002},
  pages = {335--347},
  publisher = {Springer-Verlag},
  city = {Berlin},
  series = {LNCS},
  issn = {0302-9743},
  isbn = {3-540-00029-1},
  volume = {2495},
  svrctr = {02-09},
  project = {DP0209722 CRTR},
  year = {2002},
  abstract = {We define a language and a predicative semantics 
    to model concurrent real-time programs. 
    We consider different communication pa\-ra\-digms between the
    concurrent components of a program: communication via shared variables
    and asynchronous message passing (for different models of channels).

    The semantics is the basis for a refinement calculus to derive
    machine-in\-de\-pen\-dent concurrent real-time programs from
    specifications. We give some examples of refinement laws that deal
    with concurrency.}
}
@inproceedings{TRTRCaFfMIRTP,
  author = {I. J. Hayes},
  title = {The Real-Time Refinement Calculus: A Foundation for Machine-Independent Real-Time Programming},
  booktitle = {Proceedings 23rd International Conference on the Application and Theory of Petri Nets},
  editor = {J. Esparza and C. Lakos},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  conference = { 24-30 June 2002, Adelaide, Australia},
  volume = {2360},
  pages = {44--58},
  issn = {0302-9743},
  isbn = {3-540-43787-8},
  note = {Invited keynote paper},
  code = {E1 (Invited keynote paper in refereed proceedings)},
  www = {http://www.springer.de},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {DP0209722 CRTR},
  year = {2002},
  abstract = {
    The real-time refinement calculus is an extension of the standard
    refinement calculus in which programs are developed from a
    pre-condition plus post-condition style of specification.
    In addition to adapting standard refinement rules to be valid in the
    real-time context,
    specific rules are required for the timing constructs such as delays
    and deadlines.
    Because many real-time programs may be nonterminating,
    a further extension is to allow nonterminating repetitions.

    A real-time specification constrains not only what values should
    be output,
    but when they should be output.
    Hence for a program to implement such a specification,
    it must guarantee to output values by the specified times.
    With standard programming languages such guarantees cannot be made
    without taking into account the timing characteristics of the
    implementation of the program on a particular machine.
    To avoid having to consider such details during the refinement process,
    we have extended our real-time programming language
    with a deadline command.
    The deadline command takes no time to execute and always guarantees
    to meet the specified time;
    if the deadline has already passed the deadline command is infeasible
    (miraculous in Dijkstra's terminology).
    When such a real-time program is compiled for a particular machine,
    one needs to ensure that all execution paths leading to a deadline are
    guaranteed to reach it by the specified time.
    We consider this checking as part of an extended compilation phase.
    The addition of the deadline command restores for the real-time
    language the advantage of machine independence enjoyed by
    non-real-time programming languages.}
}
@inproceedings{RaT,
  author = {I. J. Hayes},
  title = {Reasoning about Timeouts},
  booktitle = {Proc.\ Mathematics of Program Construction},
  editor = {Eerke A. Boiten and Bernhard M\"{o}ller},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  doi = {http://dx.doi.org/10.1007/3-540-45442-X_7},
  volume = {2386},
  pages = {94--116},
  issn = {0302-9743},
  isbn = {3-540-43857-2},
  www = {http://www.springer.de},
  rfcd = {280302 (Software Engineering)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  project = {A49937045 TPA/DP0209722 CRTR},
  year = {2002},
  abstract = {
    In real-time programming a timeout mechanism allows exceptional behaviour,
    such as a lack of response,
    to be handled effectively,
    while not overly affecting the programming for the normal case.
    For example, in a pump controller if the water level has
    gone below the minimum level and the pump is on and hence pumping in more
    water, then the water level should rise above the minimum level within
    a specified time.
    If not, there is a fault in the system and it should
    be shut down and an alarm raised.
    Such a situation can be handled by normal case code that determines
    when the level has risen above the minimum,
    plus a timeout case handling the situation when the specified time to
    reach the minimum has passed.

    In this paper we introduce a timeout mechanism,
    give it a formal definition in terms of more basic real-time commands,
    develop a refinement law for introducing a timeout clause to
    implement a specification,
    and
    give an example of using the law to introduce a timeout.
    The framework used is a machine-independent real-time programming
    language, which makes use of a deadline command to represent timing
    constraints in a machine-independent fashion.
    This allows a more abstract approach to handling timeouts.}
}
@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.}
}
@inproceedings{TRLPtM,
  author = {R. Colvin and I. J. Hayes and D. Hemer and P. A. Strooper},
  title = {Translating Refined Logic Programs to {Mercury}},
  booktitle = {Proceedings 25th Australasian Computer Science Conference (ACSC 2002)},
  editor = {M. Oudshoorn},
  publisher = {Australian Computer Society},
  series = {Conferences in Research and Practice in Information Technology},
  volume = {4},
  pages = {33--40},
  isbn = {0-909925-82-8},
  conference = {Melbourne, Australia},
  project = {A49937007 RefLP},
  year = {2002}
}
@inproceedings{DCOfLPR,
  author = {D. Hemer and R. Colvin and I. Hayes and P. Strooper},
  title = {Don't Care Non-Determinism in Logic Program Refinement},
  booktitle = {Proceedings of Computing: the Australasian Theory Symposium (CATS 2002)},
  editor = {J. Harland},
  publisher = {Elsevier Science},
  series = {Electronic Notes in Theoretical Computer Science (ENTCS)},
  volume = {61},
  pages = {1--21},
  isbn = {0444510850},
  conference = {Melbourne, Australia},
  project = {A49937007 RefLP},
  year = {2002},
  abstract = {
    The refinement calculus for logic programs consists of a wide-spectrum
    language, a semantics for the language and a notion of refinement that
    can be used to develop programs from specifications.
    The wide-spectrum language includes many of the concepts found in logic
    programs, including sequential composition, existential quantification,
    disjunction, procedures and recursion. A number of non-implementable
    constructs, such as universal quantification, parallel conjunction,
    assumptions and specifications, are also included.
    The semantics are defined in terms of {\em executions}, describing the
    effect of the program constructs on the state of the program.
    A notion of refinement is defined, where one program refines another if
    it terminates more often and returns the same set of answers.

    Non-determinism is supported in the language by allowing more than
    one answer, but in a refinement the refined program must return the
    same set of answers as the original program.
    In the traditional refinement calculus for imperative programs, there is
    another form of non-determinism, called {\em demonic choice}, which allows
    non-determinism to be eliminated during refinement.
    Thus, non-deterministic specifications, which give the implementer as
    much freedom as possible, can be refined to deterministic implementations.

    In this paper, we introduce a notion of demonic non-determinism into the
    refinement calculus for logic programs.
    We extend the wide-spectrum language to include demonic, non-deterministic
    choice.
    We describe the changes to the underlying semantics and the notion of
    refinement that are required, and give an example that illustrates the
    use of demonic choice.}
}
@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.}
}
@inproceedings{RCfLPiIH,
  author = {D. Hemer and I. Hayes and P. Strooper},
  title = {Refinement Calculus for Logic Programming in {Isabelle/HOL}},
  booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, {TPHOLs} 2001},
  editor = {R. Boulton and P. Jackson},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {2152},
  pages = {249--264},
  isbn = {3-540-42525-X},
  conference = {Edinburgh, Scotland},
  project = {A49937007 RefLP},
  year = {2001},
  abstract = {This paper describes a deep embedding of a
    refinement calculus for logic programs in Isabelle/HOL. It
    extends a previous tool with support for procedures and
    recursion. The tool supports refinement in context, and a
    number of window-inference tactics that ease the burden on
    the user. In this paper, we also discuss the insights
    gained into the suitability of different logics for
    embedding refinement calculii (applicable to both
    declarative and imperative paradigms). In particular, we
    discuss the richness of the language, choice between typed
    and untyped logics, automated proof support, support for
    user-defined tactics, and representation of program
    states.},
  keywords = {Refinement, logic programming, theorem provers}
}
@inproceedings{MLPR,
  author = {R. Colvin and I. J. Hayes and P. Strooper},
  title = {A Technique for Modular Logic Program Refinement},
  booktitle = {Logic-based Program Synthesis and Transformation (LOPSTR 2000) Selected Papers},
  editor = {Kung-Kiu Lau},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {2402},
  pages = {38--56},
  doi = {http://dx.doi.org/10.1007/3-540-45142-0_3},
  conference = {10th International Workshop, LOPSTR 2000},
  isbn = {3-540-42127-0},
  issn = {0302-9743},
  project = {A49937007 RefLP},
  year = {2001},
  abstract = {A refinement calculus provides a method for transforming
    specifications to executable code, maintaining the correctness of
    the code with respect to its specification.  Modules allow one to
    group together data types with sets of procedures that manipulate
    the data types.  In this paper we develop a technique for refining
    a module to one that uses a more efficient representation of the
    data type.  The technique places restrictions on the way procedures
    in the module use the data type, and on the way a program uses the
    module.  The restrictions allow a more efficient implementation to
    be developed.}
}
@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.}
}
@inproceedings{UTItMtRiaTP,
  author = {J. Shield and I. J. Hayes and D. A. Carrington},
  title = {Using Theory Interpretation to Mechanise the Reals in a Theorem Prover},
  booktitle = {Computing: The Australian Theory Symposium (CATS)},
  editor = {C. J. Fidge},
  series = {Electronic Notes in Theoretical Computer Science},
  volume = {42},
  publisher = {Elsevier Science},
  isbn = {none!},
  pages = {266--281},
  note = {URL: www.elsevier.nl/locate/entcs},
  conference = {29 Jan - 2 Feb 2001, Bond University, Gold Coast, Queensland, Australia},
  organisation = {Australian Computer Science Association},
  city = {Amsterdam},
  year = {2001}
}
@techreport{ADSfLPR-TR,
  author = {I. J. Hayes and R. Nickson and P. Strooper and R. Colvin},
  title = {A Declarative Semantics for Logic Program Refinement},
  number = {00-30},
  institution = {Software Verification Research Centre,
    The University of Queensland, Brisbane 4072, Australia},
  month = nov,
  keywords = {Logic programming, refinement.},
  project = {A49937007 RefLP},
  year = {2000},
  abstract = {The refinement calculus provides a framework for 
    the stepwise development of
    imperative programs from specifications.
    This paper presents a semantics for 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 specifications constructs
    (general predicates and assumptions) and universal quantification.
    A semantics is defined for this wide-spectrum language based on
    {\em executions}, which are partial functions from states to states,
    where a state is represented as a set of bindings.
    This execution 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 a refinement
    law for introducing recursive procedures is presented.}
}
@inproceedings{RaRTPUIIA,
  author = {I. J. Hayes},
  title = {Reasoning about Real-Time Programs Using Idle-Invariant Assertions},
  pages = {16--23},
  booktitle = {Proceedings 7th Asia-Pacific Software Engineering Conference (APSEC 2000)},
  conference = {5--8 December 2000, Singapore},
  isbn = {0-7695-0915-0},
  editor = {J. S. Dong and J. He and M. Purvis},
  publisher = {IEEE Computer Society},
  city = {Washington},
  techreport = {Also SVRC-TR-00-38},
  project = {A49801500 HertZ},
  year = {2000},
  abstract = {We develop a set of laws for reasoning about
    real-time programs using assertions (preconditions and
    postconditions) in the style of Hoare.
    In the real-time context assertions may refer to the current
    time and to the value of external inputs,
    which are not under the direct control of the program
    and hence not guaranteed to be stable with respect to the
    passage of time
    (even if the program does not modify any of the
    variables under its control).
    Hence in order to reason about real-time programs,
    we make use of idle-invariant assertions:
    assertions that are invariant to just the passage of time.}
}
@inproceedings{SRTOZS,
  author = {G. Smith and I. J. Hayes},
  title = {Structuring Real-Time {Object-Z} Specifications},
  booktitle = {IFM'00: Proceedings of the 2nd International Conference on Integrated Formal Methods},
  editor = {W. Grieskamp and T. Santen and W. J. Stoddart},
  isbn = {3-540-41196-8},
  pages = {97-115},
  series = {Lecture Notes in Computer Science},
  volume = {1945},
  publisher = {Springer},
  city = {Berlin},
  conference = {Schloss Dagstuhl, 1-3, November 2000},
  project = {A49801500 HertZ},
  year = {2000}
}
@inproceedings{RTPRuAV,
  author = {I. J. Hayes},
  title = {Real-Time Program Refinement Using Auxiliary Variables},
  pages = {170--184},
  booktitle = {Proc.\ Formal Techniques in Real-Time and Fault-Tolerant Systems},
  series = {LNCS},
  publisher = {Springer},
  volume = {1926},
  isbn = {3-540-41055-4},
  editor = {M. Joseph},
  project = {A49937045 TPA},
  year = {2000},
  abstract = {Real-time program development can be split into a
    machine-independent phase,
    that derives a machine-independent real-time
    program from a specification,
    and a machine-dependent phase,
    that checks that the compiled program will meet its
    deadlines when executed on the target machine.

    In this paper we extend a machine-independent real-time
    programming language with auxiliary variables.
    These are introduced to facilitate both reasoning about the
    correctness of real-time programs
    and the expression of timing deadlines,
    and hence
    the calculation of timing constraints on paths through a program.
    The auxiliary variable concept is extended to auxiliary
    parameters to procedures.}
}
@inproceedings{MLPR-EA,
  author = {R. Colvin and I. J. Hayes and P. Strooper},
  title = {Modular Logic Program Refinement},
  booktitle = {Pre-Proceedings of the Tenth International Workshop on
    Logic-based Program Synthesis and Transformation (LOPSTR 2000)},
  editor = {Kung-Kiu Lau},
  publisher = {Department of Computer Science, Manchester University},
  series = {Technical Report},
  number = {UMCS-00-6-1},
  pages = {1--10},
  isbn = {??},
  conference = {24--28 July 2000, Imperial College, London, UK},
  note = {Extended abstract},
  year = {2000},
  abstract = {A refinement calculus provides a method for transforming
    specifications to executable code, maintaining the correctness of
    the code with respect to its specification.  Modules allow one to
    group together data types with sets of procedures that manipulate
    the data types.  In this paper we develop a technique for refining
    a module to one that uses a more efficient representation of the
    data type.  The technique places restrictions on the way procedures
    in the module use the data type, and on the way a program uses the
    module.  The restrictions allow a more efficient implementation to
    be developed.}
}
@inproceedings{RaNtLUDC,
  author = {I. J. Hayes},
  title = {Reasoning about Non-terminating Loops Using Deadline Commands},
  pages = {60--79},
  booktitle = {Proc.\ Mathematics of Program Construction},
  isbn = {3-540-67727-5},
  issn = {0302-9743},
  editor = {R. Backhouse and J. N. Oliveira},
  series = {Lecture Notes in Computer Science},
  volume = {1837},
  note = {This paper is superseded by \cite{RaRTRTaN}},
  publisher = {Springer},
  project = {A49801500 HertZ},
  year = {2000},
  abstract = {
    It is common for a real-time process to consist of a
    nonterminating loop monitoring an input
    and controlling an output.
    Hence a real-time program development method needs to
    support nonterminating loops.
    Earlier work on real-time program development has produced a
    real-time refinement calculus that makes use of a novel
    deadline command which allows timing constraints to be
    embedded in real-time programs.
    The addition of the deadline command to the real-time
    programming language gives the significant advantage of
    providing a real-time programming language that is machine
    independent.
    This allows a more abstract approach to the program
    development process.

    In this paper we add possibly nonterminating loops to the
    refinement calculus.
    First we examine the semantics of possibly nonterminating loops,
    and use them to reason directly about a simple example.
    Then we develop simpler refinement rules that make use of a
    loop invariant.}
}
@inproceedings{RLPuT,
  author = {R. Colvin and I. J. Hayes and P. Strooper},
  title = {Refining Logic Programs Using Types},
  booktitle = {Australasian Computer Science Conference (ACSC~2000)},
  editor = {Jenny Edwards},
  publisher = {IEEE Computer Society},
  pages = {43--50},
  doi = {10.1109/ACSC.2000.824379},
  isbn = {0-7695-0518-X},
  conference = {31 Jan -- 3 Feb 2000, ANU, Canberra, Australia},
  project = {A49937007 RefLP},
  year = {2000},
  abstract = {The logic programming refinement calculus is a method for
    transforming specifications to executable code, maintaining the
    correctness of the code with respect to its specification.  In this paper
    we show how types can be handled in the logic programming refinement
    calculus.  Types of variables are necessary for a complete specification
    of a procedure, and typing information can guide the refinement of a
    procedure specification to code.  As an application of this framework,
    we show how dynamic type-checks can be formally eliminated from a
    sample program.}
}
@inproceedings{RTSaRUMI,
  author = {C. J. Fidge and I. J. Hayes and B. P. Mahony and A. K. Wabenhorst},
  title = {Real-Time Specification and Reasoning Using Maximal Intervals},
  editor = {W. C. H. Cheng and A. S. M. Sajeev},
  booktitle = {PART'99: Proceedings of the 6th Australasian Conference on Parallel and Real-Time Systems},
  pages = {344--354},
  isbn = {981-4021-59-8},
  publisher = {Springer},
  year = {1999}
}
@inproceedings{TRTOZ,
  author = {G. Smith and I. J. Hayes},
  title = {Towards Real-Time {Object-Z}},
  booktitle = {IFM'99: Proceedings of the 1st International Conference on Integrated Formal Methods},
  editor = {Keijiro Araki and Andy Galloway and Kenji Taguchi},
  isbn = {1-85233-107-0},
  pages = {49--65},
  publisher = {Springer},
  city = {London},
  conference = {York, 28--29 June 1999},
  project = {A49801500 HertZ},
  year = {1999}
}
@incollection{SaNNE99,
  author = {I. J. Hayes and C. B. Jones},
  title = {Specifications are not (necessarily) executable},
  booktitle = {High-Integrity System Specification and Design},
  editor = {J. P. Bowen and M. G. Hinchey},
  isbn = {3-540-76226-4},
  note = {(Previously published in {\em IEE/BCS Software Engineering Journal},
  Vol.\ 4, No.\ 6, 330--338, November, 1989)},
  pages = {563--581},
  publisher = {Springer},
  city = {London},
  project = {A49801500 HertZ},
  year = {1999}
}
@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}
}
@inproceedings{DDaIiZ,
  author = {C. J. Fidge and I. J. Hayes and B. P. Mahony},
  title = {Defining Differentiation and Integration in {Z}},
  booktitle = {Proceedings Second International Conference on Formal Engineering Methods ({ICFEM'98})},
  editor = {J. Staples and M. G. Hinchey and {Shaoying Liu}},
  isbn = {0-8186-9198-0},
  pages = {64--73},
  publisher = {IEEE Computer Society},
  svrctr = {UQ-SVRC-98-09},
  where = {Brisbane, Australia},
  year = {1998}
}
@inproceedings{STaCiRTR,
  author = {I. J. Hayes},
  title = {Separating timing and calculation in real-time refinement},
  booktitle = {Int.\ Refinement Workshop and Formal Methods Pacific 1998},
  editor = {J. Grundy and M. Schwenke and T. Vickers},
  publisher = {Springer},
  isbn = {981-4021-16-4},
  pages = {1--16},
  pdf = {../Papers/rtsep.pdf},
  city = {Singapore},
  svrctr = {UQ-SVRC-98-14},
  year = {1998},
  abstract = {
    We consider the specification and refinement of sequential
    real-time programs.
    Our real-time specifications describe the allowable behaviours
    of an implementation in terms of the values of variables over time.
    Hence within a specification the values of the variables and
    the times at which they have those values are intertwined.
    However, in a real-time program some commands are concerned
    with calculating the right outputs, while other commands,
    such as delays and deadlines, are concerned with making sure
    the outputs appear at the right time.
  
    During the refinement process we would like to decompose the
    overall problem into those aspects dealing with time and
    those that are purely calculation.
    We need refinement rules that allow us to separate these
    concerns.
    Further, given a component that is only concerned with
    calculation, the complexities of the real-time calculus that
    deal with timing behaviour are an unnecessary burden.
    Such calculational components can be developed more
    straightforwardly in the standard refinement calculus.
    We would like to allow the use of the untimed calculus for
    the development of such components.
    To do that we need to embed the untimed calculus within the
    real-time calculus.}
}
@inproceedings{SCitSRTRC,
  author = {L. P. Wildman and I. J. Hayes},
  title = {Supporting Contexts in the Sequential Real-Time Refinement Calculus},
  booktitle = {International Refinement Workshop and Formal Methods Pacific 1998},
  editor = {J. Grundy and M. Schwenke and T. Vickers},
  publisher = {Springer},
  isbn = {981-4021-16-4},
  pages = {352--369},
  svrctr = {UQ-SVRC-98-29},
  city = {Singapore},
  year = {1998}
}
@inproceedings{DRLP,
  author = {R. Colvin and I. J. Hayes and P. Strooper},
  title = {Data refining logic programs},
  booktitle = {International Refinement Workshop and Formal Methods Pacific 1998},
  editor = {J. Grundy and M. Schwenke and T. Vickers},
  series = {Discrete Mathematics and Theoretical Computer Science},
  publisher = {Springer},
  isbn = {981-4021-16-4},
  pages = {100--116},
  city = {Singapore},
  svrctr = {UQ-SVRC-98-15},
  project = {A49937007 RefLP},
  year = {1998},
  abstract = {
    A refinement calculus provides a method for transforming
    specifications to executable code, maintaining the correctness of the
    code with respect to its specification.  One aspect of refinement is
    transforming the representation of data in a specification.  This could
    be performed for efficiency reasons, or to change an abstract specification
    type into a data type that is in the target implementation language.
    This paper looks at data refinement in the refinement calculus for logic
    programs.  Three cases for data refinement in the logic calculus are
    examined, and the process for each is described.  The three cases
    are illustrated by a running example.}
}
@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}
}
@inproceedings{mpc98,
  author = {C. J. Fidge and I. J. Hayes and A. P. Martin and A. K. Wabenhorst},
  title = {A Set-Theoretic Model for Real-Time Specification and Reasoning},
  editor = {J. Jeuring},
  booktitle = {Mathematics of Program Construction (MPC'98)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 1422,
  pages = {188--206},
  comment = {Also available as SVRC TR 98-07},
  project = {A49801500 HertZ},
  year = 1998
}
@inproceedings{DaT,
  author = {I. J. Hayes and M. Utting},
  title = {Deadlines are Termination},
  booktitle = {IFIP TC2/WG2.2, 2.3 International Conference on
  Programming Concepts and Methods (PROCOMET'98)},
  conference = {8--12 June 1998, Shelter Island, New York, USA},
  editor = {D. Gries  and  W.-P. de Roever},
  isbn = {0-412-83760-9},
  pages = {186--204},
  pdf = {../Papers/procomet.pdf},
  publisher = {Chapman and Hall},
  city = {London},
  year = {1998}
}
@inproceedings{TCA98,
  author = {S. Grundon and I. J. Hayes and C. J. Fidge},
  title = {Timing Constraint Analysis},
  booktitle = {Computer Science '98: Proc.\ 21st Australasian Computer Sci.\ Conf.\ ({ACSC'98})},
  location = {{\rm Perth, 4--6 Feb.}},
  editor = {C. McDonald},
  publisher = {Springer},
  pages = {575--586},
  year = {1998}
}
@inproceedings{RefLP-Tool-NFMW,
  author = {R. Colvin and I. J. Hayes and R. Nickson and P.  A. Strooper},
  title = {A Tool for Logic Program Refinement},
  booktitle = {Second {BCS-FACS} Northern Formal Methods Workshop (NFMW'97)},
  other = {Ilkley, UK, July, 1997},
  editor = {D. J. Duke and A. S. Evans},
  isbn = {3-540-76215-9},
  series = {Electronic Workshops in Computing},
  publisher = {Springer},
  city = {London},
  project = {A49937007 RefLP from small grant},
  year = {1997}
}
@inproceedings{BancroftHayesTypeExtensionandRefinement,
  author = {P. G. Bancroft and I. J. Hayes},
  title = {Type extension and refinement},
  pages = {23--39},
  editor = {L. Groves and S. Reeves},
  booktitle = {Formal Methods Pacific (FMP'97)},
  publisher = {Springer},
  isbn = {981-3083-31-X},
  city = {Singapore},
  year = {1997},
  abstract = {This paper extends the methods of the refinement
    calculus to allow the derivation of certain kinds of Oberon-like
    programs. The use of records, pointers, opaque types and type
    extension distinguishes the work from previous examples.
    A case study for a queue abstract data type illustrates a method
    for the derivation of a generic, linked implementation.
    Firstly, a sequence of integers is refined to a sequence of
    integer records with link pointers. The the sequence of records
    is refined to a generic linked list that is close to Oberon code.
    Pointers are facilitated by declaring an explicit local data
    store for each queue variable. The advantage of Oberon over
    Modula-2 is the ability to separate the final code into two
    modules - a generic queue that maintains the linked data
    structure invariant and an integer instantiation of the queue,
    using type extension. This separation of concerns (isolation of
    the linked data structure properties) is the main benefit of the
    approach.}
}
@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.}
}
@inproceedings{CoercingRTR,
  author = {I. J. Hayes and M. Utting},
  title = {Coercing real-time refinement: A transmitter},
  booktitle = {{BCS-FACS} Northern Formal Methods Workshop (NFMW'96)},
  other = {Ilkley, UK, September, 1996},
  editor = {D. J. Duke and A. S. Evans},
  isbn = {3-540-76117-9},
  pdf = {../Papers/trco.pdf},
  series = {Electronic Workshops in Computing},
  publisher = {Springer},
  city = {London},
  year = {1997}
}
@inproceedings{LOPSTR-LP,
  author = {I. Hayes and R. Nickson and P. Strooper},
  title = {Refining specifications to logic programs},
  editor = {J. Gallagher},
  booktitle = {Logic Program Synthesis and Transformation.  Proc.\ of the 6th Int.\ Workshop, LOPSTR'96, Stockholm, Sweden, August 1996},
  volume = {1207},
  pages = {1--19},
  series = {Lecture Notes in Computer Science},
  isbn = {3-540-62718-9},
  uqcall = {QA76 .L4 v.1207},
  publisher = {Springer},
  project = {A49937007 RefLP from small grant},
  year = {1997}
}
@proceedings{ARW96,
  title = {Proc.\ 5th Australasian Refinement Workshop},
  editor = {I. J. Hayes},
  organization = {Software Verification Research Centre, The University of Queensland},
  note = {Unrefereed.},
  url = {http://www.itee.uq.edu.au/~arw},
  month = {April},
  year = {1996}
}
@inproceedings{ARW96-LP,
  author = {I. J. Hayes and P. A. Strooper},
  title = {Refining specifications to logic programs},
  booktitle = {Proc.\ 5th Australasian Refinement Workshop},
  editor = {I.J. Hayes},
  pages = {1--13},
  publisher = {Software Verification Research Centre, The University of Queensland},
  note = {Unrefereed.},
  url = {http://www.itee.uq.edu.au/MENU/WORKSHOPS-SEMINARS-CONFERENCES/WORKSHOPS/5thaus.html},
  month = {April},
  project = {A49937007 RefLP},
  year = {1996}
}
@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}
}
@inproceedings{PRT:TOOL-PAPER,
  author = {D. A. Carrington and I. J. Hayes and R. Nickson and G. Watson and J. Welsh},
  title = {A Tool for Developing Correct Programs by Refinement},
  booktitle = {Proc.\ BCS 7th Refinement Workshop, Bath, UK},
  editor = {{He Jifeng}},
  series = {Electronic Workshops in Computing},
  publisher = {Springer},
  pages = {1--17},
  project = {PRT},
  year = {1996}
}
@inproceedings{FidgeUttingKearneyHayes96,
  author = {C. J. Fidge and M. Utting and P. Kearney and I. J. Hayes},
  title = {Integrating real-time scheduling theory and program refinement},
  editor = {M.-C. Gaudel and J. Woodcock},
  booktitle = {FME'96: Industrial Benefit and Advances in Formal Methods},
  proctitle = {Proc.\ Formal Methods Europe ({FME'96})},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  pages = {327--346},
  volume = {1051},
  year = {1996}
}
@inproceedings{FidgeUttingHayesKearney96,
  author = {C. J. Fidge and M. Utting and I. J. Hayes and P. Kearney},
  title = {The {Quartz} refinement method for real-time multi-tasking systems},
  booktitle = {Fifth Australasian Refinement Workshop (ARW'96)},
  month = apr,
  city = {Brisbane},
  year = {1996}
}
@inproceedings{Presentation-of-proofs96,
  author = {D. A. Carrington and I. J. Hayes and R. Nickson and G. Watson and J. Welsh},
  title = {Structured Presentation of Refinements and Proofs},
  booktitle = {Proc.\ 19th Australasian Computer Science Conference ({ACSC'96})},
  editor = {Kotagiri Ramamohanarao},
  series = {Australian Computer Science Communications},
  volume = {18(1)},
  pages = {87--96},
  month = {February},
  project = {PRT},
  year = {1996}
}
@inproceedings{talp-95,
  title = {The communicating technologist: An educational challenge},
  author = {P. Bakker and D.A. Carrington and A. Goodchild and I.J. Hayes
    and H. Purchase and P.A. Strooper},
  booktitle = {Frontiers in Education 25th Annual Conference},
  editor = {D. Budny and B. Herrick},
  pages = {4a4.1--4a4.4},
  publisher = {IEEE Press},
  address = {Atlanta, Georgia},
  year = 1995
}
@inproceedings{Hayes-spec-models,
  author = {I. J. Hayes},
  title = {Specification Models},
  booktitle = {Proc.\ 7th International Conference on
    Putting into Practice Methods and Tools for Information Systems Design,
    10--12 October, 1995, Nantes},
  note = {Invited keynote paper.},
  pages = {1--10},
  month = oct,
  year = {1995}
}
@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}
}
@inproceedings{BancroftHayes-type-ext,
  author = {P. Bancroft and I. J. Hayes},
  title = {A Formal Semantics for a Language with Type Extension},
  booktitle = {ZUM'95: The Z Formal Specification Notation, Proc.\ 9th International Conference of Z Users, Limerick, Ireland, September 7--9, 1995},
  isbn = {3-540-60271-2},
  series = {Lecture Notes in Computer Science},
  volume = {967},
  publisher = {Springer},
  pages = {299--314},
  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}
}
@inproceedings{RfaPRE,
  author = {David Carrington and Ian Hayes and Ray Nickson and Geoffrey Watson and Jim Welsh},
  title = {Requirements for a Program Refinement Engine},
  booktitle = {Proc.\ of the 4th Australasian Refinement Workshop (ARW'95)},
  pages = {67--83},
  publisher = {School of Computer Science and Engineering, University of New South Wales},
  month = apr,
  project = {PRT},
  year = {1995}
}
@techreport{Tutoring,
  author = {Report of the Computer Science Action Learning Group},
  title = {Improving the Quality of Tutorial Classes in Computer Science},
  institution = {Department of Computer Science, University of Queensland},
  number = {UQ-CS-322},
  year = {1995}
}
@inproceedings{WildmanHayes:UQ2comp,
  author = {L. P. Wildman and I. J. Hayes},
  key = {Z modularity UQ2 grammar composition},
  title = {Composing grammar transformations to construct a specification of a parser},
  booktitle = {Proc.\ 18th Australasian Computer Science Conference ({ACSC'95}), Glenelg, South Australia, Australian Computer Science Communications},
  editor = {Ramamohanarao Kotagiri},
  pages = {556--562},
  pdf = {../Papers/composing_trans.pdf},
  journal = {Australian Computer Science Communications},
  volume = {17(1)},
  month = {February},
  year = {1995},
  abstract = {As part of a project with the aim of scaling up formal
    methods, we have developed a library construct for the
    specification language Z.  This paper reports on the result
    of using libraries to structure a specification of a
    relatively complicated parser for a language-based editor.
    The parser is complicated by the need to cope with multiple
    languages as well as tolerate errors in the input.
    
    Our goal in producing the specification of the parser has
    been to separate each of the major concepts on which the
    specification is based (eg, multiple languages and
    error-tolerance) into a separate library.
    
    To achieve the separation of concerns we have applied  the
    novel technique of specifying each of the major concepts of
    the parser as grammar transformations. The full parser can
    then be specified by composing the separate transformations
    to give a grammar incorporating all the desired features.}
}
@inproceedings{boiler-overview,
  author = {B. P. Mahony and C. Millerchip and I. J. Hayes},
  title = {A boiler control system:
            Overview of a case study in timed refinement},
  booktitle = {Software Safety: Everybody's Business,
    Proceedings of the 1993 International Invitational Workshop on
    Design and Review of Software-Controlled Safety-Related Systems,
    Ottawa},
  editor = {Diana Del Bel Belluz and Herbert C. Ratz},
  key = {realtime specification refinement boiler},
  publisher = {The Institute of Risk Research},
  city = {Waterloo, Canada},
  pages = {189--208},
  year = {1994}
}
@inproceedings{boiler-full,
  author = {B. P. Mahony and C. Millerchip and I. J. Hayes},
  title = {A boiler control system:
            A case study in timed refinement},
  booktitle = {Technical proceedings International Symposium on Design and Review of Software-Controlled Safety-Related Systems, Ottawa},
  editor = {Diana Del Bel Belluz},
  ps = {../Papers/boilerdesign.ps},
  key = {realtime specification refinement boiler},
  note = {50 pages},
  month = {June},
  year = {1993}
}
@inproceedings{PWI-ARW,
  author = {Ray Nickson and Ian Hayes},
  title = {Program Window Inference},
  booktitle = {Proc.\ of the 4th Australasian Refinement Workshop (ARW'95)},
  pages = {43--65},
  publisher = {School of Computer Science and Engineering, University of New South Wales},
  note = {Unrefereed. Also available as Technical Report UQ-SVRC-95-29, Software Verification Research Centre, University of Queensland},
  month = apr,
  project = {PRT},
  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}
}
@techreport{Diff-VDM-Z-TR,
  author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
  title = {Understanding the differences between {VDM} and {Z}},
  institution = {Department of Computer Science, University of Manchester},
  type = {Technical report},
  number = {UMCS-93-8-1},
  ps = {../Papers/UMCS-93-8-1.ps},
  month = {August},
  year = {1993}
}
@inproceedings{DMDfFS:93,
  author = {D. A. Carrington and D. Duke and I.  J. Hayes and J. Welsh},
  title = {Deriving Modular Designs from Formal Specifications},
  booktitle = {{Int.\ Symp.\ on the Foundations of Software Engineering (SIGSOFT'93)}},
  location = {Los Angeles},
  isbn = {0-89791-625-5},
  publisher = {ACM},
  pages = {89--98},
  pdf = {../Papers/tr93-06.pdf},
  year = {1993}
}
@book{SCS2,
  editor = {I. J. Hayes},
  title = {Specification Case Studies},
  edition = {second},
  publisher = {Prentice Hall},
  isbn = {0-13-832544-8},
  acquired = {30 March 1993},
  pdf = {../Papers/SCS2.pdf},
  year = {1993}
}
@incollection{SCS2-eg,
  author = {I. J. Hayes},
  booktitle = {Specification Case Studies},
  edition = {second},
  editor = {I. J. Hayes},
  pages = {2--13},
  publisher = {Prentice Hall International},
  title = {Examples of specification using mathematics},
  year = {1993}
}
@incollection{SCS2-bst,
  author = {I. J. Hayes},
  booktitle = {Specification Case Studies},
  edition = {second},
  editor = {I. J. Hayes},
  pages = {14--30},
  publisher = {Prentice Hall International},
  title = {Block-structured symbol table},
  year = {1993}
}
@incollection{SCS2-flexi,
  author = {I. J. Hayes},
  booktitle = {Specification Case Studies},
  edition = {second},
  editor = {I. J. Hayes},
  pages = {134--138},
  publisher = {Prentice Hall International},
  title = {Flexitime specification},
  year = {1993}
}
@incollection{SCS2-cics,
  author = {I. J. Hayes},
  booktitle = {Specification Case Studies},
  edition = {second},
  editor = {I. J. Hayes},
  note = {(Previously published in IEEE Transactions on Software Engineering \cite{Hayes85a})},
  pages = {181--201},
  publisher = {Prentice Hall International},
  title = {Applying formal specification to software development in industry},
  year = {1993}
}
@incollection{SCS2-ts,
  author = {I. J. Hayes},
  booktitle = {Specification Case Studies},
  edition = {second},
  editor = {I. J. Hayes},
  pages = {226--237},
  publisher = {Prentice Hall International},
  title = {{CICS} temporary storage},
  year = {1993}
}
@incollection{SCS2-mess,
  author = {I. J. Hayes},
  booktitle = {Specification Case Studies},
  edition = {second},
  editor = {I. J. Hayes},
  pages = {238--243},
  publisher = {Prentice Hall International},
  title = {{CICS} message system},
  year = {1993}
}
@inproceedings{BancroftHayes:RaMwOT,
  author = {P. Bancroft and I. J. Hayes},
  booktitle = {Proceedings, 16th Australian Computer Science Conference, Brisbane, Australian Computer Science Communications},
  editor = { Gopal Gupta and George Mohay and Rodney Topor},
  title = {Refining a Module with Opaque Types},
  journal = {Australian Computer Science Communications},
  volume = {15(1)},
  pages = {615--624},
  month = {February},
  year = {1993}
}
@inproceedings{HayesWildman:zmod,
  pdf = {../Papers/zmod.pdf},
  author = {I. J. Hayes and L. P. Wildman},
  booktitle = {Z User Workshop: Proceedings of the Seventh Annual {Z} User Meeting, London, December 1992},
  editor = {J. P. Bowen and J. E. Nicholls},
  key = {Z modularity},
  publisher = {Springer},
  title = {Towards Libraries for {Z}},
  series = {Workshops in Computing},
  pages = {37--51},
  isbn = {3-540-19818-0},
  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
}
@inproceedings{WardHayes91a,
  author = {N. Ward and I. J. Hayes},
  booktitle = {Proc.\ 6th Australian Software Engineering Conference (ASWEC91)},
  editor = {P. A. Bailes},
  pages = {391--404},
  publisher = {Australian Computer Society},
  title = {Applications of Angelic Nondeterminism},
  pdf = {../Papers/ASWEC91-Ward-Hayes.pdf},
  city = {Sydney},
  month = jul,
  category = {M},
  year = {1991}
}
@inproceedings{MahonyHayes91b,
  author = {B. P. Mahony and I. J. Hayes},
  booktitle = {Proc.\ 6th Australian Software Engineering Conf.\ (ASWEC91)},
  editor = {P. A. Bailes},
  pages = {257--270},
  publisher = {Australian Comp.\ Soc.},
  title = {Using continuous real functions to model timed histories},
  pdf = {../Papers/mahony91continuity.pdf},
  city = {Sydney},
  category = {M},
  year = {1991}
}
@inproceedings{MahonyHayes91a,
  author = {B. P. Mahony and I. J. Hayes},
  booktitle = {Proc.\ BCS/FACS Fourth Refinement Workshop},
  publisher = {Springer},
  title = {A case study in timed refinement: A central heater},
  city = {Cambridge},
  pages = {138--149},
  pdf = {../Papers/mahony91heater.pdf},
  series = {Workshops in Computing},
  month = jan,
  year = {1991}
}
@incollection{Hayes90e,
  author = {I. J. Hayes},
  booktitle = {System and Software Requirements Engineering},
  editor = {Richard H. Thayer and Merlin Dorfman},
  note = {(Previously published in IEEE Transactions on Software Engineering \cite{Hayes85a})},
  annote = {This paper was selected for inclusion in the tutorial by the editors},
  pages = {594--603},
  publisher = {IEEE Computer Society Press Tutorial},
  title = {Applying Formal Specification to Software Development in Industry},
  year = 1990
}
@inproceedings{Hayes90d,
  author = {I. J. Hayes},
  booktitle = {Z User Workshop: Proceedings of the Fifth Annual {Z} User Meeting, Oxford, December 1990},
  key = {Z schema operators},
  publisher = {Springer},
  title = {Interpretations of {Z} schema operators},
  series = {Workshops in Computing},
  pages = {12--26},
  year = {1991}
}
@inproceedings{CarringtonHayesWelsh90,
  author = {D. A. Carrington and I. J. Hayes and J. Welsh},
  booktitle = {Proc.\ of Pacific TOOLS '90},
  key = {Z object oriented},
  title = {A Syntax-Directed Editor for Object-Oriented Specifications},
  pages = {46--57},
  city = {Sydney},
  month = nov,
  year = {1990}
}
@techreport{Hayes90b-TR,
  author = {I. J. Hayes},
  institution = {Department of Computer Science, University of Queensland},
  title = {Specifying Physical Limitations: A Case Study of an Oscilloscope},
  type = {Technical report},
  number = {167},
  month = {July},
  pages = {17 pages},
  ps = {../Papers/TR0167.ps},
  year = 1990
}
@inproceedings{HayesNeucomWelsh89,
  author = {I. J. Hayes and R. Neucom and J. Welsh},
  booktitle = {Advance papers CASE'89},
  city = {London},
  key = {Z language},
  title = {An Editor for {Z} Specifications},
  pages = {1--13},
  year = {1989}
}
@inproceedings{Hayes89a,
  author = {I. J. Hayes},
  booktitle = {Z User Workshop: Proceedings of the Fourth Annual {Z} User Meeting, Oxford, December 1989},
  editor = {J. E. Nicholls},
  key = {Z language bags},
  publisher = {Springer},
  city = {London},
  title = {A generalisation of bags in {Z}},
  series = {Workshops in Computing},
  uqcall = {QA76.73.Z2},
  pages = {113--127},
  year = {1990}
}
@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}
}
@inproceedings{HayesMowbrayRose89,
  author = {I. J. Hayes and M. Mowbray and G. A. Rose},
  booktitle = {Protocol Specification, Testing and Verification, {IX}},
  editor = {E. Brinksma and G. Scollo and C. A. Vissers},
  pages = {3--14},
  title = {{Signalling System No. 7}: The Network Layer},
  publisher = {Elsevier Science Publishers B. V.  (North-Holland)},
  year = {1990}
}
@techreport{HayesNeucomWelsh88,
  author = {I. J. Hayes and R. Neucom and J. Welsh},
  title = {An editor for {Z} specifications},
  pages = {13 pages},
  institution = {Department of Computer Science, University of Queensland},
  year = {1988}
}
@inproceedings{DukeHayesKingRose88,
  author = {R. Duke and I. J. Hayes and P. King and G. A. Rose},
  booktitle = {IFIP Eighth International Workshop on Protocol Specification, Testing and Verification},
  pages = {33--46},
  title = {Protocol Specification and Verification Using {Z}},
  publisher = {North-Holland},
  year = {1988}
}
@techreport{DukeHayesRose88,
  author = {R. Duke and I. J. Hayes and G. A. Rose},
  title = {Verification of a cyclic retransmission protocol},
  number = {UQ-CS-92},
  pages = {1--23},
  institution = {Department of Computer Science, The University of Queensland},
  month = {July},
  year = {1988}
}
@inproceedings{HoareHayesEtcFull92,
  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},
  title = {Laws of Programming},
  booktitle = {Programming and Mathematical Method},
  editor = {Manfred Broy},
  series = {NATO ASI Series F: Computer and Systems Sciences},
  volume = {88},
  key = {Marktoberdorf 1990},
  pages = {95-122},
  publisher = {Springer},
  isbn = {3-540-55558-7},
  year = {1992}
}
@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}
}
@book{Hayes87a,
  editor = {I. J. Hayes},
  key = {book editor cics distributed computing caviar icl data dictionary unix file},
  pages = {332 pages},
  publisher = {Prentice Hall International},
  title = {Specification Case Studies},
  year = {1987}
}
@inproceedings{Hayes87h,
  address = {Canberra},
  author = {I. J. Hayes},
  booktitle = {Proc.\ 2nd Australian Software Engineering Conference (ASWEC-87)},
  key = {Z language},
  month = may,
  dates = {13--15 May},
  pages = {75--86},
  publisher = {IREE (Australia)},
  title = {Correctness of data representations},
  year = {1987}
}
@inproceedings{RoseDukeHayes87,
  address = {Canberra},
  author = {G. A. Rose and R. Duke and I. J. Hayes},
  booktitle = {Proc 2nd Australian Software Engineering Conference (ASWEC-87)},
  key = {Z language},
  month = may,
  dates = {13--15 May},
  pages = {161--170},
  publisher = {IREE (Australia)},
  title = {Specifying communications services and protocols},
  year = {1987}
}
@techreport{HayesRobinson87,
  address = {Brisbane, Australia},
  author = {I. J. Hayes and K. A. Robinson},
  institution = {Department of Computer Science, University of Queensland},
  pages = {35 pages},
  title = {A {Modula}-2-Based Translator Generator},
  type = {Technical report 84},
  year = {1987}
}
@inproceedings{Hayes86c,
  address = {Canberra},
  author = {I. J. Hayes},
  booktitle = {Proc.\ 1st Australian Software Engineering Conference (ASWEC-86)},
  key = {z specification language},
  month = may,
  dates = {14--16 May},
  pages = {67--71},
  publisher = {Institution of Engineers, Australia},
  title = {Using mathematics to specify software},
  note = {At the 10th ASWEC Conference in 1997 this paper was given the
    award of {\em Most Influential Paper of ASWEC'86}, the
    first ASWEC Conference},
  pdf = {../Papers/aswec.pdf},
  year = {1986}
}
@inproceedings{Hayes86b,
  address = {Canberra},
  author = {I. J. Hayes},
  booktitle = {Proc.\ 9th Australian Computer Science Conference},
  month = jan,
  conference = {29--31 January},
  pages = {299--308},
  title = {Weakest pre-specifications: weakest pre-conditions for procedures},
  year = {1986}
}
@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}
}
@phdthesis{Hayes83,
  address = {Sydney, Australia},
  author = {I. J. Hayes},
  pages = {261 pages},
  school = {Department of Computer Science, University of New South Wales},
  title = {Computer Architecture: The hardware/software interface},
  type = {{Ph.\ D.} Thesis},
  year = {1983}
}
@techreport{HayesRobinson82,
  address = {Sydney, Australia},
  author = {I. J. Hayes and K. A. Robinson},
  institution = {Department of Computer Science, University of New South Wales},
  pages = {27 pages},
  title = {A Tutorial on {Llama}: A {Pascal}-Based Translator Generator},
  type = {Technical report},
  year = {1982}
}

This file was generated by bibtex2html 1.99.

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