Machine-Assisted Reasoning about Concurrency and Dynamic Memory (2009)
Keith Bauer, Lindsay Groves, Ray Nickson
The project is concerned with machine-assisted reasoning about non-blocking concurrent algorithms involving dynamic data structures. We present PVS formalisms for reasoning about concurrency based on...
Andrew Martin, Andrew Martin, Ray Nickson, Ray Nickson, Mark Utting, Mark Utting
reports are available via anonymous ftp, from svrc.it.uq.edu.au in the directory /pub/techreports. Abstracts and compressed postscript files are available via
Lindsay Groves Ray, Ray Nickson, Greg Reeve, Steve Reeves, Mark Utting
. We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with...
A Declarative Semantics for Logic Program Renement (2007)
Robert Colvin, Ian Hayes, Ian Hayes, Ray Nickson, Ray Nickson, Paul Strooper, ...
Note: Most SVRC technical reports are available via anonymous ftp, from svrc.it.uq.edu.au in the directory /pub/techreports. Abstracts and compressed postscript les are available via
Developing logic programs from specifications using stepwise refinement (2004)
Robert Colvin, Lindsay Groves, Ian J. Hayes, David Hemer, Ray Nickson, Paul Strooper
This chapter was by invitation as part of the "State-of-the-Art" survey in logic program development. It is a summary of work performed as a PhD student and as a research officer.
Developing logic programs from specifications using stepwise refinement (2004)
Robert Colvin, Lindsay Groves, Ian J. Hayes, David Hemer, Ray Nickson, Paul Strooper
This chapter was by invitation as part of the "State-of-the-Art" survey in logic program development. It is a summary of work performed as a PhD student and as a research officer.
Developing logic programs from specifications using stepwise refinement (2004)
Colvin, Robert, Groves, Lindsay, Hayes, Ian J., Hemer, David, Nickson, Ray, Strooper, Paul
In this paper we demonstrate a refinement calculus for logic programs, which is a framework for developing logic programs from specifications. The paper is written in a tutorial-style, using a...
Developing logic programs from specifications using stepwise refinement (2004)
Colvin, Robert, Groves, Lindsay, Hayes, Ian J., Hemer, David, Nickson, Ray, Strooper, Paul
In this paper we demonstrate a refinement calculus for logic programs, which is a framework for developing logic programs from specifications. The paper is written in a tutorial-style, using a...
Ergo 6: a generic proof engine that uses Prolog proof technology (2002)
Utting, Mark, Robinson, Peter, Nickson, Ray
This paper describes the architecture of the Ergo theorem prover. It discusses the use of Prolog technology as the implementation language. The paper provides a useful comparison of this technology...
A refinement calculus for logic programs (2002)
Ian Hayes, Robert Colvin, David Hemer, Paul Strooper, Ray Nickson
TPLP is a Tier 1 journal. My contribution to this paper was as a PhD student.
A Refinement Calculus for Logic Programs (2002)
Hayes, Ian, Colvin, Robert, Hemer, David, Strooper, Paul, Nickson, Ray
Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The...
Ergo 6: a generic proof engine that uses Prolog proof technology (2002)
Utting, Mark, Robinson, Peter, Nickson, Ray
This paper describes the architecture of the Ergo theorem prover. It discusses the use of Prolog technology as the implementation language. The paper provides a useful comparison of this technology...
Machine-Assisted Reasoning about Concurrency and Dynamic Memory (2001)
Keith Bauer, Supervisor Lindsay Groves, Ray Nickson
Submitted in partial fulfilment of the requirements for
A Declarative Semantics for Logic Program Refinement (2000)
Hayes, Ian, Nickson, Ray, Strooper, Paul, Colvin, Robert
The refinement calculus provides a framework for the stepwise development of imperative programs from specifications. This paper presents a semantics for a refinement calculus for deriving logic...
A survey of software development practices in the New Zealand software industry (2000)
Groves, Lindsay, Nickson, Ray, Reeve, Greg, Reeves, Steve, Utting, Mark
We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a...
A survey of software development practices in the New Zealand software industry (2000)
Groves, Lindsay, Nickson, Ray, Reeve, Greg, Reeves, Steve, Utting, Mark
We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a...
A Declarative Semantics for Logic Program Refinement (2000)
Hayes, Ian, Nickson, Ray, Strooper, Paul, Colvin, Robert
The refinement calculus provides a framework for the stepwise development of imperative programs from specifications. This paper presents a semantics for a refinement calculus for deriving logic...
A Declarative Semantics for Logic Program Refinement (2000)
Hayes, Ian, Nickson, Ray, Strooper, Paul, Colvin, Robert
The refinement calculus provides a framework for the stepwise development of imperative programs from specifications. This paper presents a semantics for a refinement calculus for deriving logic...
Groves, Lindsay, Nickson, Ray, Reeve, Greg, Reeves, Steve, Utting, Mark
We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a...
Groves, Lindsay, Nickson, Ray, Reeve, Greg, Reeves, Steve, Utting, Mark
We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a...
Lindsay Groves, Ray Nickson, Greg Reeve, Steve Reeves, Mark Utting
Abstract. We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software...
A Tool for Refining Logic Programs (1997)
Robert Colvin, Robert Colvin, Ian Hayes, Ian Hayes, Ray Nickson, Ray Nickson, ...
The refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In the original refinement...
A Tactic Language for Ergo (1997)
Andrew Martin, Andrew Martin, Ray Nickson, Ray Nickson, Mark Utting, Mark Utting
A new version of the Ergo theorem prover is under development. It uses a single tactic language, based on Angel, for tactic programming, user interface, and proof representation. This paper describes...
Interpretation and Instantiation of Theories for Reasoning about Formal Specifications (1997)
Nicholas Hamilton, Nicholas Hamilton, Ray Nickson, Ray Nickson, Owen Traynor, ...
In this paper an outline is given of an approach to formally reasoning about importation, parameterisation and instantiation of specifications written in a modular extension of the Z language (called...
Supporting Contexts in Program Refinement (1996)
Ray Nickson, Ray Nickson, Ian Hayes, Ian Hayes
A program can be refined either by transforming the whole program or by refining one of its components. The refinement of a component is, for the main part, independent of the remainder of the...
Ergo 4.1 Reference Manual (1996)
Holger Becht, Holger Becht, Anthony Bloesch, Anthony Bloesch, Ray Nickson, Ray Nickson, ...
This document describes the commands available in the theorem prover Ergo. It assumes that the reader is familiar, to some extent, with Ergo (refer to the Ergo User Manual [UW94]). As such, it is...
David Carrington, David Carrington, Ian Hayes, Ian Hayes, Ray Nickson, Ray Nickson, ...
Refinement is a mathematically-based technique for developing a program from an abstract specification so that the program satisfies the specification. The aim of the Program Refinement Tool project...
A New Face For Ergo: Adding A User Interface To A Programmable Theorem Prover (1995)
Ray Nickson, Ray Nickson, Mark Utting, Mark Utting
We describe some of the technology we used to build a user interface for a programmable theorem prover. By separating the user interface from the application itself, it is possible to experiment with...
Program Window Inference (1995)
Ray Nickson, Ray Nickson, Ian Hayes, Ian Hayes
A program can be refined either by transforming the whole program or by refining one of its components. The refinement of a component is, for the main part, independent of the remainder of the...
Requirements for a Program Refinement Engine (1995)
David Carrington, David Carrington, Ian Hayes, Ian Hayes, Ray Nickson, Ray Nickson, ...
Refinement is a mathematically-based technique for developing a program from an abstract specification so that the program satisfies the specification. The aim of the Program Refinement Tool project...
A Review of Existing Refinement Tools (1994)
David Carrington, David Carrington, Ian Hayes, Ian Hayes, Ray Nickson, Ray Nickson, ...
This report examines the requirements for a support tool for the stepwise refinement of program specifications to program code using the refinement calculus. This calculus, which was developed...
A Declarative Semantics for Logic Program Refinement
Hayes, Ian, Nickson, Ray, Strooper, Paul, Colvin, Robert
The refinement calculus provides a framework for the stepwise development of imperative programs from specifications. This paper presents a semantics for a refinement calculus for deriving logic...