@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{DistributiveLaws,
author = {Larissa A. Meinicke and Ian J. Hayes},
title = {Reasoning about distributive laws in a concurrent refinement algebra},
booktitle = {The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part II},
editor = {A. Cavalcanti and J. Baxter},
publisher = {Springer Nature Switzerland},
address = {Cham},
volume = {14781},
series = {Lecture Notes in Computer Science},
pages = {1--22},
url = {https://doi.org/10.1007/978-3-031-66673-5_1},
doi = {10.1007/978-3-031-66673-5_1},
abstract = {Distributive laws are important for algebraic reasoning in arithmetic and logic.
They are equally important for algebraic reasoning about concurrent programs.
In existing theories such as Concurrent Kleene Algebra, only partial correctness is handled,
and many of its distributive laws are weak,
in the sense that they are only refinements in one direction, rather than equalities.
The focus of this paper is on strengthening our theory to support
the proof of strong distributive laws that are equalities,
and in doing so come up with laws that are quite general.
Our concurrent refinement algebra supports total correctness
by allowing both finite and infinite behaviours.
It supports the rely/guarantee approach of Jones
by encoding rely and guarantee conditions as rely and guarantee commands.
The strong distributive laws may then be used to distribute rely and guarantee commands
over sequential compositions and into (and out of) finite iterations.
They may also be used to distribute other commands,
such as commands that specify a termination requirement,
a fairness requirement, an evolution invariant, and a generalised invariant,
in exactly the same way.
Strong (equality) distributive laws are essential for handling data refinement of concurrent programs.},
project = {DP190102142 DV4CS},
year = {2024}
}
@inproceedings{RaCRA,
author = {Hayes, Ian J. and Meinicke, Larissa A. and Evangelou-Oost, Naso},
editor = {Fahrenberg, Uli and Fussner, Wesley and Gl{\"u}ck, Roland},
title = {Restructuring a Concurrent Refinement Algebra},
booktitle = {Relational and Algebraic Methods in Computer Science},
publisher = {Springer Nature Switzerland},
address = {Cham},
volume = {14787},
series = {Lecture Notes in Computer Science},
pages = {135--155},
abstract = {The concurrent refinement algebra has been developed to support rely/guarantee reasoning about concurrent programs. The algebra supports atomic commands and defines parallel composition as a synchronous operation, as in Milner's SCCS. In order to allow specifications to be combined, the algebra also provides a weak conjunction operation, which is also a synchronous operation that shares many properties with parallel composition. The three main operations, sequential composition, parallel composition and weak conjunction, all respect a (weak) quantale structure over a lattice of commands. Further structure involves combinations of pairs of these operations: sequential/parallel, sequential/weak conjunction and parallel/weak conjunction, each pair satisfying a weak interchange law similar to Concurrent Kleene Algebra. Each of these pairs satisfies a common biquantale structure. Additional structure is incorporated in the form of compatible sets of commands, including tests and atomic commands. These facilitate stronger (equality) interchange and distributive laws. This paper describes the result of restructuring the algebra to better exploit these commonalities. The algebra is implemented in Isabelle/HOL.},
isbn = {978-3-031-68279-7},
project = {DP190102142 DV4CS},
year = {2024}
}
@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 (RAMiCS 2023)},
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{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{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{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{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{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{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{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{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{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{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 16 Oct 2024 10:29:59 AEST
