INPROCEEDINGS.bib

@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib -ob INPROCEEDINGS.bib -oc INPROCEEDINGS-cites -c 'not $key : "TRX$"' -c '$type : "^INPROCEEDINGS$"' ../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}
}
@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 = {}
}
@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 = {}
}
@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}
}
@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 = {}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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
}
@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.}
}
@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.}
}
@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}
}
@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.}
}
@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.}
}
@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}
}
@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.}
}
@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.}
}
@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.}
}
@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}
}
@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}
}
@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.}
}
@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.}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}

This file was generated by bibtex2html 1.99.

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