ABZ2008 Conference - Short Papers (2008)
Boerger, Egon, Butler, Michael, Bowen, Jonathan, Boca, Paul
Short papers of the ABZ 2008 Conference September 16-18, 2008 BCS London Offices, Covent Garden, London, UK Full published proceedings in Springer LNCS Vol. 5238:...
y A simple `shallow ' semantic embedding of the Z notation into the higher order logic, as supported by the HOL theorem proving system, is presented. Z is is typically used for human-readable...
ESPRIT Working Group 8694 A ProCoS-WG Working Group Final Report: ESPRIT Working Group 8694 (2007)
Jonathan Bowen, Hans Langmaack, Ernst-rüdiger Olderog, Anders P. Ravn
P r o v a b l y C o r r e c t
Hardware Compilation of the ProCoS Gas Burner Case Study using Logic Programming (2007)
A hardware compiler may bespeci ed by a description of how each construct of the source language is translated into a netlist of simple digital hardware components such as gates and latches....
The Internet worldwide computer network of networks provides an unparalleled opportunity for organizations ranging from individuals to multinational companies to make information rapidly and easily...
The World Wide Web (WWW) has been expanding exponentially since it was launched. It provides a unifying way tonavigate and present information around the world in seconds using the Internet computer...
KEY WORDS Field Programmable Gate Arrays (FPGAs) Hardware compilation Logic programming (2007)
The use of Field Programmable Gate Arrays (FPGA) to rapidly produce custom hardware circuits using a completely software-based process is becoming increasingly widespread. Specialized Hardware...
TowardsaProvably Correct Hardware Implementation of Occam (2007)
Abstract. This paper shows how to compile a program written in a subset of occam into a normal form suitable for further processing into a netlist of components which may be loaded into a...
Address for correspondence: (2007)
Jonathan P. Bowen, Michael K. Houghton, Jonathan Bowen, Berks Rg Ay
The dramatic increase in the popularity of the Internet, largely brought about by the World Wide Web, has significantly increased the need for environments to support remote collaboration, learning,...
Jonathan Bowen, Jonathan Bowen, Jonathan Bowen, Jonathan Bowen, Victoria Stavridou, Victoria Stavridou, ...
Standards concerned with the development of safety-critical systems, and the software in such systems in particular, abound today as the software crisis increasingly a ects the world of embedded...
He Jifeng, Jonathan Bowen, Paritosh Pandya
A compiler is speci ed by a description of how each construct of the source language is translated into a sequence of object code instructions. The meaning of the object code can be de ned by...
c1993BCS Speci cation, Veri cation and Prototyping of an Optimized Compiler (2007)
This paper generalizes an algebraic method for the design of a correct compiler to tackle speci cation and veri cation of an optimized compiler. The main optimization issues of concern here include...
A Shallow Embedding of Z in HOL (2007)
A simple ‘shallow ’ semantic embedding of the Z notation into the higher order logic, as supported by the HOL theorem proving system, is presented. Z is is typically used for human-readable...
Jonathan Bowen, Jonathan Bowen, Victoria Stavridou, Victoria Stavridou
Standards concerned with the development of safety-critical systems, and the software in such systems in particular, abound today as the software crisis increasingly a ects the world of embedded...
Jonathan Bowen, Peter Breuer, Jonathan Bowen Y, Peter Breuer Z
This guide gives some information about Oxford, particularly for visitors to the Programming Research Group. It was originally written for two collaborative ESPRIT projects, so some parts are...
A simple `shallow ' semantic embedding of the Z notation into the HOL logic is described. The Z notation is based on set theory and rst order predicate logic and is typically used for...
Procos Ii, Jonathan Bowen, Hans Langmaack, Ernst-rudiger Olderog, Anders P. Ravn
P r o v a b l y C o r r e c t
Unu Iist Report, Jonathan Bowen, Jonathan Bowen
Eclogue: The logic programming language Prolog is used to provide a rapid-prototype simulator for the VERILOG Hardware Description Language (HDL). The simulator is based on an operational semantics...
The FACS FACTS Team Newsletter Editor Paul Boca (2006)
Editorial Team, Jonathan Bowen, Judith Carlton, John Cooke, Kevin Lano, Cliff Jones, ...
FACS FACTS [ISSN: 0950-1231] is the newsletter of the BCS Specialist
Contributors to this Issue (2005)
Editorial Team, Jonathan Bowen, Judith Carlton, John Cooke, Kevin Lano, ...
FACS FACTS [ISSN: 0950-1231] is the newsletter of the BCS Specialist
The FACS FACTS Team Newsletter Editor Paul Boca (2005)
Editorial Team, Jonathan Bowen, Judith Carlton, John Cooke, Kevin Lano, Mike Stannett, ...
FACS FACTS [ISSN: 0950-1231] is the newsletter of the BCS Specialist
The FACS FACTS Team Newsletter Editor Paul Boca [ (2004)
Editorial Team, Jonathan Bowen, Judith Carlton, John Cooke, Kevin Lano, Mike Stannett, ...
FACS FACTS [ISSN: 0950-1231] is the newsletter of the BCS Specialist
FACS FACTS Issue 2004-3 25 Years of CSP (2004)
Teresa Numerico, Jonathan Bowen
conference was held to celebrate the 25 th anniversary of the introduction of Tony Hoare’s programming language CSP (Communicating Sequential Processes) [1]. The language, designed to facilitate...
Museophile: A Community for Museum E-commerce (2002)
Large national museums can afford to create their own on-line mass communication services and to undertake e-commerce activities themselves. However, for other museums, this can be a daunting...
Museophile: A Community for Museum E-commerce (2002)
Large national museums can afford to create their own on-line mass communication services and to undertake e-commerce activities themselves. However, for other museums, this can be a daunting...
Museophile: A Community for Museum E-commerce (2002)
Large national museums can afford to create their own on-line mass communication services and to undertake e-commerce activities themselves. However, for other museums, this can be a daunting...
WWW Virtual Library: Formal Methods (1999)
Formal Methods Virtual Library is a division of WWW Virtual Library [http://www.vlib.org/]. This document contains some pointers to information on Formal Methods available around the world on the...
WWW Virtual Library: Logic Programming (1999)
Logic Programming Virtual Library is a division of WWW Virtual Library [http://www.vlib.org/]. This document contains some pointers to information on Logic Programming available around the world on...
WWW Virtual Library: Safety-Critical Systems (1999)
Safety-Critical Systems Virtual Library is a division of WWW Virtual Library [http://www.vlib.org/]. This page contains pointers to information on Safety-Critical Systems, where human lives may be at...
WWW Virtual Library: Audio (1999)
Audio Virtual Library is a division of WWW Virtual Library [http://www.vlib.org/]. This document contains some pointers to information on computer-based audio sound and associated software available...
Formal Methods Meetings (1999)
This web site contains some pointers to meetings involved with formal methods for which on-line information is available on the World Wide Web.
WWW Virtual Library: Formal Methods (1999)
Formal Methods Virtual Library is a division of WWW Virtual Library [http://www.vlib.org/]. This document contains some pointers to information on Formal Methods available around the world on the...
WWW Virtual Library: Logic Programming (1999)
Logic Programming Virtual Library is a division of WWW Virtual Library [http://www.vlib.org/]. This document contains some pointers to information on Logic Programming available around the world on...
WWW Virtual Library: Safety-Critical Systems (1999)
Safety-Critical Systems Virtual Library is a division of WWW Virtual Library [http://www.vlib.org/]. This page contains pointers to information on Safety-Critical Systems, where human lives may be at...
WWW Virtual Library: Audio (1999)
Audio Virtual Library is a division of WWW Virtual Library [http://www.vlib.org/]. This document contains some pointers to information on computer-based audio sound and associated software available...
Formal Methods Meetings (1999)
This web site contains some pointers to meetings involved with formal methods for which on-line information is available on the World Wide Web.
Networked Multi-user and Multimedia Environments for Learning and Collaboration (1999)
Jonathan Bowen, Berks Rg Ay, Jonathan P. Bowen, Michael K. Houghton
The dramatic increase in the popularity of the Internet, largely brought about by the World Wide Web, has significantly increased the need for environments to support remote collaboration, learning,...
Animating the Semantics of VERILOG using Prolog (1999)
Jonathan Bowen, Jonathan Bowen
Portugal through contribution to the UNU Endowment Fund. The mission of UNU/IIST is to assist developing countries in the application and development of software technology. UNU/IIST contributes...
Networked Multi-user and Multimedia Environments (1999)
For Learning And, Jonathan Bowen, Berks Rg Ay, Jonathan P. Bowen, Michael K. Houghton
The dramatic increase in the popularity of the Internet, largely brought about by the World Wide Web, has significantly increased the need for environments to support remote collaboration, learning,...
Networked Multi-user and Multimedia Environments for Learning and Collaboration (1999)
Jonathan Bowen, Berks Rg Ay, Jonathan P. Bowen, Michael K. Houghton
The dramatic increase in the popularity of the Internet, largely brought about by the World Wide Web, has significantly increased the need for environments to support remote collaboration, learning,...
KEY WORDS Field Programmable Gate Arrays (FPGAs) Hardware compilation Logic programming (1999)
The use of Field Programmable Gate Arrays (FPGA) to rapidly produce custom hardware circuits using a completely software-based process is becoming increasingly widespread. Specialized Hardware...
Jonathan Bowen, Jonathan Bowen
Portugal through contribution to the UNU Endowment Fund. The mission of UNU/IIST is to assist developing countries in the application and development of software technology. UNU/IIST contributes...
The Virtual Library museums pages (VLmp): Whence and whither (1997)
The Virtual Library museums pages (VLmp) were started as a personal project in 1994, forming part of the Virtual Library distributed information repository initiated by the original inventors of the...
Jonathan Bowen, Jonathan Bowen Y
This bibliography contains a list of Z references that are either available as published papers, books or technical reports from institutions, or from the author, the Programming Research Group (PRG)...
Jonathan Bowen, Jonathan Bowen, Jonathan Bowen
This document gives an up-to-date list of Z references. A version of this bibliography
Jonathan Bowen, Jonathan Bowen, Jonathan Bowen
This document gives an up-to-date list of Z references. A version of this bibliography is due appear in the Proceedings of the Z User Workshop, York 1991, edited by John Nicholls, in the...
Jonathan Bowen, Susan Stepney, Rosalind Barden
This annotated Z bibliography contains a selected list of some pertinent publications for Z users. Most of those included are readily available, either as books or in journals. A few unpublished...
Formal Methods in Safety-Critical Standards (1994)
There is great interest in ensuring correctness of safety-critical embedded systems since on the one hand the use of software gives greatly increased functionality and exibility and on the other hand...
Jonathan Bowen, Michael R. Hansen, Anders P. Ravn, Hans Rischel, Ernst-rudiger Olderog, ...
r r e c
Formal Methods in Safety-Critical Standards (1994)
Jonathan Bowen, Andrew Tanenbaum
There is great interest in ensuring correctness of safety-critical embedded systems since on the one hand the use of software gives greatly increased functionality and flexibility and on the other...
Formal Speci cations in Software Maintenance: From code to Z ++ and back again (1993)
Jonathan Bowen, Peter Breuer, Kevin Lano
This paper presents a numberoftechniques that have been developed as components of the software maintenance process as part of the ESPRIT REDO project. These techniques are all based on formal...
The Industrial Take-up of Formal Methods in Safety-Critical and Other Areas: A Perspective (1993)
Jonathan Bowen, Victoria Stavridou
Abstract. Formal methods may be at the crossroads of acceptance by a wider industrial community. In order for the techniques to become widely used, the gap between theorists and practitioners must be...
Programs to Object Code and back again using Logic Programming: Compilation and Decompilation (1993)
languageistranslatedintoasequenceofobjectcodeinstructions.Itispossibleto produceacompilerprototypealmostdirectlyfromthisspecicationintheformofa...
Safety-critical systems, formal methods and standards (1993)
Jonathan Bowen, Jonathan Bowen, Victoria Stavridou, Victoria Stavridou
Standards concerned with the development of safety-critical systems, and the software in such systems in particular, abound today as the software crisis increasingly affects the world of embedded...
A ProCoS II Project Description: ESPRIT Basic Research project 7071 (1993)
An overview of the current and planned activities of the ESPRIT Basic Research ProCoS II project (no. 7071) on "Provably Correct Systems" is presented. This is a follow-on project to ProCoS...
Jonathan Bowen, Jonathan Bowen
This bibliography contains a list of Z references that are either available as published papers, books or technical reports from institutions, or from the author, the Programming Research Group (PRG)...
Safety-Critical Systems, Formal Methods and Standards (1993)
Jonathan P. Bowen, Jonathan Bowen, Jonathan Bowen, Jonathan Bowen, Victoria Stavridou, Victoria Stavridou, ...
Standards concerned with the development of safety-critical systems, and the software in such systems in particular, abound today as the software crisis increasingly affects the world of embedded...
Towards Verified Systems OVERVIEW (1993)
Jonathan Bowen, Jonathan Bowen (ed
This memory is a function from names to values (i.e. numbers). Inputs too are modelled by functions from names to values. It is assumed that at each moment the environment specifies a value ' i...
Time interval semantics and implementation of a real-time programming language (1992)
This paper presents a real-time programming language, including concurrency, which could be usedin the formal development of embedded systems. The semantics of the language is provided in the form of...
From programs to object code using logic and logic programming (1992)
A compiler may be speci ed by a description of how each construct of the source language is translated into a sequence of object code instructions. If the machine that interprets the object code is...
Time interval semantics and implementation of a real-time programming language (1992)
This paper presents a real-time programming language, including concurrency, which could be used in the formal development of embedded systems. The semantics of the language is provided in the form...
From programs to object code using logic and logic programming (1992)
A compiler may be specified by a description of how each construct of the source language is translated into a sequence of object code instructions. If the machine that interprets the object code is...
Occam's Razor: The Cutting Edge for Parser Technology (1992)
Jonathan Bowen, Peter T. Breuer
Yacc is well established in the compiler-compiler field, but is beginning to show its age. Issues which were important when hardware resources were more scarce are now less critical. Precc is a new...
Jonathan Bowen, He Jifeng, Paritosh Pandya Z
Acompilermaybespeciedasasetoftheorems,eachdescribinghowaconstructinthe programminglanguageistranslatedintoasequenceofmachineinstructions.Themachinemay...
Esprit bra 3104 procos project: Provably correct systems (1990)
He Jifeng, Jonathan Bowen, Paritosh Pandya
Summary A compiler is specified by a description of how each construct of the source language is translated into a sequence of object code instructions. The meaning of the object code can be defined...
The Aliens' Guide to Oxford (1990)
Jonathan P. Bowen, Jonathan Bowen, Peter T. Breuer, Peter Breuer
This guide gives some information about Oxford, particularly for visitors to the Programming Research Group. It was originally written for two collaborative ESPRIT projects, so some parts are...
User interface languages: A survey of existing methods (1989)
Jonathan Bowen, Alan Dix, Gregory Abowd, Gregory Abowd, Jonathan Bowen Y, Alan Dix Z, ...
University ofYork
User Interface Languages: A Survey of Existing Methods (1989)
Gregory Abowd, Gregory Abowd, Jonathan P. Bowen, Jonathan Bowen, Alan Dix, Alan Dix, ...
This report gives a survey of user interface languages and formal representations of user interfaces. The following aspects of User Interface Languages are considered: expressiveness; readability;...
User interface languages: A survey of existing methods (1989)
Jonathan Bowen, Alan Dix, Gregory Abowd, Gregory Abowd, Jonathan Bowen Y, Alan Dix Z, ...
University ofYork
THE ETHICS OF SAFETY-CRITICAL SYSTEMS. (0000)
This article focuses on the use of software in safety-critical systems This article focuses on the use of software in safety-critical systems. Computers are used in safety- critical...
THE ETHICS OF SAFETY-CRITICAL SYSTEMS.
This article focuses on the use of software in safety-critical systems This article focuses on the use of software in safety-critical systems. Computers are used in safety- critical...
The World Wide Web and the Virtual Library museums pages
The World Wide Web (WWW) has been expanding exponentially since it was launched. It provides a unifying way to navigate and present information around the world in seconds using the Internet computer...