TECHREPORT.bib

@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bib2bib -ob TECHREPORT.bib -oc TECHREPORT-cites -c 'not $key : "TRX$"' -c '$type : "^TECHREPORT$"' ../pubs-html.bib}}
@techreport{HayesJonesColvin14TR,
  author = {Ian J. Hayes and Cliff B. Jones and Robert J. Colvin},
  title = {Laws and Semantics for Rely-Guarantee Refinement},
  institution = {School of Computing Science, Newcastle University},
  numpages = {66},
  note = {Superseded by \cite{FMJournalAtomicSteps-TR} and other papers. 66 pages},
  number = {CS-TR-1425},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT/LP0989643 SPA},
  keywords = {rely-guarantee, concurrency},
  abstract = {
    Interference is the essence of concurrency and it is what makes reasoning about concurrent programs difficult.
    The fundamental insight of rely-guarantee thinking is that stepwise design of concurrent programs can only be
    compositional in development methods that offer ways to record and reason about interference.
    In this way of thinking, a rely relation records assumptions about the behaviour of the environment,
    and a guarantee relation records commitments about the behaviour of the process.
    The standard application of these ideas is in the extension of Hoare-like inference rules to quintuples
    that accommodate rely and guarantee conditions.
    In contrast, in this paper, we embed rely-guarantee thinking into a refinement calculus for concurrent programs,
    in which programs are developed in (small) steps from an abstract specification.
    As is usual, we extend the implementation language with specification constructs
    (the extended language is sometimes called a wide-spectrum language),
    in this case adding two new commands:
      a guarantee command $(\mathbf{guar} g ~\cdot~c)$ whose valid behaviours are in accord with the command $c$
      but all of whose atomic steps also satisfy the relation $g$,
      and a rely command $(\mathbf{rely} r ~\cdot~c)$ whose behaviours are like $c$ provided
      any interference steps from the environment satisfy the relation $r$.
      The theory of concurrent program refinement is based on a theory of atomic program steps and
      more powerful refinement laws, most notably,
      a law for decomposing a specification into a parallel composition,
      are developed from a small set of more primitive lemmas,
      which are proved sound with respect to an operational semantics.
  },
  month = jul,
  year = {2014}
}
@techreport{RRGT-TR13,
  author = {Ian J. Hayes and Cliff B. Jones and Robert J. Colvin},
  title = {Reasoning about concurrent programs: Refining rely-guarantee thinking},
  institution = {School of Computing Science, Newcastle University},
  numpages = {66},
  note = {Superseded by CS-TR-1425. 66 pages},
  number = {CS-TR-1395},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP130102901 RGT/LP0989643 SPA},
  keywords = {rely-guarantee, concurrency},
  abstract = {
    Interference is the essence of concurrency and it is what makes
    reasoning about concurrent programs difficult.
    The fundamental insight of rely-guarantee thinking is that stepwise design of 
    concurrent programs can only be compositional in development methods that
    offer ways to record and reason about interference.
    In this way of thinking, a \emph{rely} relation records assumptions about
    the behaviour of the \emph{environment}, and a \emph{guarantee} relation records
    commitments about the behaviour of the \emph{process}.  The standard
    application of these ideas is in the extension of 
    Hoare-like inference rules to quintuples that accommodate rely and guarantee conditions. 
    In contrast, in this paper, we embed rely-guarantee thinking
    into a refinement calculus for concurrent programs, in which programs are
    developed in (small) steps from an abstract specification.
    As is usual, we extend the implementation language with specification
    constructs (the extended language is sometimes called a wide-spectrum
    language), in this case adding (in addition to pre and postconditions) 
    two new commands:
    a guarantee command $(\mathbf{guar} g ~\cdot~ c)$ whose valid behaviours are in accord with the command $c$ 
    but all of whose atomic steps also satisfy the relation $g$,
    and 
    a rely command $(\mathbf{rely} r ~\cdot~ c)$ whose behaviours are like $c$ provided 
    any interference steps from the environment satisfy the relation $r$.
    The theory of concurrent program refinement is based on a 
    theory of atomic program steps and more
    powerful refinement laws, most notably, a law for decomposing a
    specification into a parallel composition, are developed from a small
    set of more primitive lemmas, which are proved sound with respect to an
    operational semantics.
  },
  month = sep,
  year = {2013}
}
@techreport{CMoNEE-TR,
  author = {I. J. Hayes and A. Burns and B. Dongol and C. B. Jones},
  title = {Comparing Models of Non\-deterministic Expression Evaluation},
  institution = {School of Computing Science, Newcastle University},
  pages = {1--21},
  number = {CS-TR-1273},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  keywords = {sampling logic},
  abstract = {
    Expression evaluation in programming languages is normally
    deterministic; however, if expressions involve variables that are
    being modified by the environment of the process during their
    evaluation, the result of the evaluation can be non\-deterministic.
    Two common cases where this occurs are in concurrent programs
    where processes share variables and real-time programs that
    interact to monitor and/or control their environment.
    In these contexts, while any particular evaluation of an expression
    gives a single result, there is a range of possible results that
    could be returned depending on the relative timing of modification
    of variables by the environment and their access within expression
    evaluation.
    Hence to model the semantics of expression evaluation one can use
    the set of possible values the expression evaluation could return.
    This paper considers three views of interpreting expressions
    nondeterministically.
    The paper formalises the three approaches,
    highlights different properties satisfied by the approaches,
    relates the approaches
    and
    explores conditions under which they coincide.
    Furthermore, a link is made to a new notation used in reasoning about interference.
  },
  month = {September},
  year = {2011}
}
@techreport{timebands-TR,
  author = {Alan Burns and Kun Wei and Jim Woodcock and Ian J. Hayes and Cliff B. Jones},
  title = {Timebands Framework -- 2011},
  number = {YCS-2011-467},
  pages = {1--36},
  note = {36 pages},
  institution = {Department of Computer Science, University of York},
  for = {080309 (Software Engineering)},
  seo = {890299 (Computer Software and Services not elsewhere classified)},
  project = {DP0987452 TFTR},
  abstract = {Complex real-time systems must integrate physical processes with digital control,
    human operation and organisational structures. New scientific foundations are
    required for specifying, designing and implementing these systems. One key challenge
    is to cope with the wide range of time scales and dynamics inherent in such
    systems. To exploit the unique properties of time, with the aim of producing more
    dependable computer-based systems, a timeband framework has been developed.
    In this paper we review this framework and report on modifications, extensions
    and applications that have been undertaken in funded research that completed in
    2011.},
  year = {2011}
}
@techreport{TSftOGTIwtPLfU07-TR,
  author = {Brijesh Dongol and Ian J. Hayes},
  title = {Trace Semantics for the {Owicki-Gries} Theory Integrated with the Progress Logic from UNITY},
  number = {SSE-2007-02},
  institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
  year = {2007}
}
@techreport{ASfBT-TR,
  author = {R. Colvin and I.J. Hayes},
  title = {A Semantics for Behavior Trees},
  institution = {ARC Centre for Complex Systems (ACCS)},
  type = {ACCS Technical Report},
  number = {ACCS-TR-07-01},
  url = {http://www.accs.edu.au/documents/TechnicalReports/ACCS_TR_07_01},
  month = {April},
  project = {CEO348249 ACCS},
  year = {2007}
}
@techreport{BurnsEt05,
  author = {A. Burns and I. J. Hayes and G. Baxter and C. J. Fidge},
  title = {Modelling Temporal Behaviour in Complex Socio-Technical Systems},
  year = {2005},
  institution = {University of York},
  url = {https://www.cs.york.ac.uk/rts/publications/Burns2005.html},
  pdf = {../Papers/R_Burns_2005.pdf},
  number = {YCS~390}
}
@techreport{BaFICBE05,
  author = {Cook, Phil and Welsh, Jim and Hayes, Ian J.},
  title = {Building a Flexible Incremental Compiler Back-End},
  number = {SSE-2005-02},
  institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
  year = {2005}
}
@techreport{ISEfIS05,
  author = {Cook, Phil and Welsh, Jim and Hayes, Ian J.},
  title = {Incremental Semantic Evaluation for Interactive Systems: Inertia, Pre-emption, and Relations},
  number = {SSE-2005-01},
  institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland},
  year = {2005}
}
@techreport{ICSEiC-TR,
  author = {Phil Cook and Jim Welsh and Ian J. Hayes},
  title = {Incremental Context-Sensitive Evaluation in Context},
  institution = {Software Verification Research Centre, The University of
    Queensland},
  number = {02-11},
  project = {Phil PhD},
  year = {2002}
}
@techreport{BSAG-TR,
  author = {Ian J. Hayes},
  title = {Block-Structured (Attribute) Grammars},
  institution = {Software Verification Research Centre, The University of Queensland},
  number = {02-47},
  month = dec,
  project = {},
  code = {K (Research report)},
  rfcd = {280303 (Programming Languages)},
  seo = {700199 (Computer Software and Services n.e.c.)},
  year = {2002},
  abstract = {
    Most computing languages are highly structured but
    conventional (flat) grammars
    do not make that structure explicit.
    To address this issue, we examine adding block structure
    to grammars.
    We allow a production in a grammar to have local productions
    associated with it.
    The local productions are accessible only via that production.
    Local productions for one construct may be nested within
    local productions for higher level constructs to form a
    tree-structured hierarchy.

    If block structuring is used with an attribute grammar one
    can also avoid explicit copying of inherited attributes
    through intermediate nodes in the parse tree that do not
    modify or make use of the attribute.
    For example, in the definition of an expression in a
    programming language grammar one may have an environment
    attribute that is identical for all nodes in the expression
    subtree.
    The explicit passing down of the environment attribute
    through the intermediate nodes
    can be avoided by allowing direct reference to the
    environment attribute of the top-level expression
    nonterminal.
  },
  keywords = {Block structure; attribute grammars; L-attribute grammars; 
    upward remote attributes.}
}
@techreport{ADSfLPR-TR,
  author = {I. J. Hayes and R. Nickson and P. Strooper and R. Colvin},
  title = {A Declarative Semantics for Logic Program Refinement},
  number = {00-30},
  institution = {Software Verification Research Centre,
    The University of Queensland, Brisbane 4072, Australia},
  month = nov,
  keywords = {Logic programming, refinement.},
  project = {A49937007 RefLP},
  year = {2000},
  abstract = {The refinement calculus provides a framework for 
    the stepwise development of
    imperative programs from specifications.
    This paper presents a semantics for a refinement calculus for deriving 
    logic programs.
    The calculus contains a wide-spectrum logic programming language, 
    including
    executable constructs such as sequential conjunction, disjunction, and
    existential quantification, as well as specifications constructs
    (general predicates and assumptions) and universal quantification.
    A semantics is defined for this wide-spectrum language based on
    {\em executions}, which are partial functions from states to states,
    where a state is represented as a set of bindings.
    This execution semantics is used to define the meaning of programs and
    specifications, including parameters and recursion.
    To complete the calculus, a notion of correctness-preserving refinement 
    over programs in the wide-spectrum language is defined and a refinement
    law for introducing recursive procedures is presented.}
}
@techreport{Tutoring,
  author = {Report of the Computer Science Action Learning Group},
  title = {Improving the Quality of Tutorial Classes in Computer Science},
  institution = {Department of Computer Science, University of Queensland},
  number = {UQ-CS-322},
  year = {1995}
}
@techreport{Diff-VDM-Z-TR,
  author = {I. J. Hayes and C. B. Jones and J. E. Nicholls},
  title = {Understanding the differences between {VDM} and {Z}},
  institution = {Department of Computer Science, University of Manchester},
  type = {Technical report},
  number = {UMCS-93-8-1},
  ps = {../Papers/UMCS-93-8-1.ps},
  month = {August},
  year = {1993}
}
@techreport{Hayes90b-TR,
  author = {I. J. Hayes},
  institution = {Department of Computer Science, University of Queensland},
  title = {Specifying Physical Limitations: A Case Study of an Oscilloscope},
  type = {Technical report},
  number = {167},
  month = {July},
  pages = {17 pages},
  ps = {../Papers/TR0167.ps},
  year = 1990
}
@techreport{HayesNeucomWelsh88,
  author = {I. J. Hayes and R. Neucom and J. Welsh},
  title = {An editor for {Z} specifications},
  pages = {13 pages},
  institution = {Department of Computer Science, University of Queensland},
  year = {1988}
}
@techreport{DukeHayesRose88,
  author = {R. Duke and I. J. Hayes and G. A. Rose},
  title = {Verification of a cyclic retransmission protocol},
  number = {UQ-CS-92},
  pages = {1--23},
  institution = {Department of Computer Science, The University of Queensland},
  month = {July},
  year = {1988}
}
@techreport{HayesRobinson87,
  address = {Brisbane, Australia},
  author = {I. J. Hayes and K. A. Robinson},
  institution = {Department of Computer Science, University of Queensland},
  pages = {35 pages},
  title = {A {Modula}-2-Based Translator Generator},
  type = {Technical report 84},
  year = {1987}
}
@techreport{HayesRobinson82,
  address = {Sydney, Australia},
  author = {I. J. Hayes and K. A. Robinson},
  institution = {Department of Computer Science, University of New South Wales},
  pages = {27 pages},
  title = {A Tutorial on {Llama}: A {Pascal}-Based Translator Generator},
  type = {Technical report},
  year = {1982}
}

This file was generated by bibtex2html 1.99.

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