Model Checking for Stability Analysis in Rely-Guarantee Proofs (2009)
Abstract. Rely-guarantee (RG) reasoning is useful for modular Hoare-style proofs of concurrent programs. However, RG requires that assertions be proved stable under the actions of the environment. We...
advantage, the copyright notice above and the title of the book appear, and notice is given
found at the ENTCS Macro Home Page. Variables as Resource in Separation Logic (2008)
Richard Bornat, Cristiano Calcagno, Hongseok Yang
Replace this file with prentcsmacro.sty for your meeting,
A Cyclic Termination Proof of In-Place List Reversal using Separation Logic (2008)
James Brotherston, Richard Bornat, Cristiano Calcagno
Abstract. We give a cyclic termination proof, based upon separation logic, for the classical imperative program performing in-place reversal of a “frying-pan ” linked list segment (so called...
Abstract Local reasoning, separation and aliasing (2008)
Structures built by pointer aliasing, such as DAGs and graphs, are notoriously tricky to deal with. The mechanisms of separation logic can deal with these structures, but so far this has been done by...
Septe Mb Er, Bernard Sufrin, Richard Bornat
In this note we show how Jape's presentations of proofs are related to the natural-deduction presentations used by Jim Woodcock and Jim Davies in [7] ("the book"). This is followed by...
Using J'n'J in Unix/X JAPE: Natural Deduction using the Jape Proof Editor (2007)
Bernard Sufrin, Richard Bornat
In this note we describe, by means of a number of case studies, the user interface to the Jape implementation -- "J'n'J" -- of the logic described in [7] ("the book")....
Animating Operational Semantics with (2007)
Bernard Sufrin Richard, Richard Bornat
In this note we give a brief introduction to the ideas of operational semantics and show how to use Jape to animate the operational semantics of a couple of simple programming languages. We give the...
Vectorising a Non-Strict Data-Parallel Functional Language (2007)
Jonathan Hill, Keith M. Clarke, Richard Bornat
The role of a vectorising compiler for an imperative language is to transform the for-loops of a program into the vector instructions of a data-parallel machine. In a functional language, constant...
1 Getting Started with J'n'J (2007)
Bernard Sufrin, Richard Bornat
In this note we describe, by means of a number of case studies, the user interface to the Jape implementation { \J'n'J " { of the logic described in [7] (\the book"). The...
Animating Operational Semantics with Jape (2007)
Bernard Sufrin, Richard Bornat
In this note we give a brief introduction to the ideas of operational semantics and show how to use Jape to animate the operational semantics of a couple of simple programming languages. We give the...
J'n'J in Jape Encoding a Natural Deduction System for the Jape Proof Editor (2007)
Bernard Sufrin, Richard Bornat
In this note we show how Jape's presentations of proofs are related to the naturaldeduction presentations used by Jim Woodcock and Jim Davies in [7] (\the book"). This is followed by...
hour talks, two invited short courses and forty-eight contributed papers. There were also (2007)
Richard Bornat, The Dov Gabbay, Wilfrid Hodges, Martin Hyl, Thomas Jech, David Makinson, ...
demonstrations of computerized logic teaching software, by Stephen Read, Steve Reeves
Abstract Program Logic and Equivalence in the Presence of Garbage Collection ⋆ (2007)
Cristiano Calcagno, Richard Bornat, Queen Mary
It is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over memory....
Local Reasoning, Separation and Aliasing (2007)
Richard Bornat School, Richard Bornat
Structures built by pointer aliasing, such as DAGs and graphs, are notoriously tricky to deal with. The mechanisms of separation logic can deal with these structures, but so far this has been done by...
Permission Accounting in Separation Logic (Extended Abstract) (2007)
Richard Bornat, Cristiano Calcagno, Peter O'Hearn, Matthew Parkinson
Separation logic began by describing total separation between the heap space used by separate parts of a program. It has moved on to consider how total and partial permissions to access heap elements...
Modular verification of a non-blocking stack. (2007)
Bornat, Richard, Parkinson, Matthew, O'Hearn, Peter
This paper contains a model and a proof of soundness for a range of program logics based on separation logic and including the notions of permission and ownership for stack variables. It shows that...
Modular verification of a non-blocking stack. (2007)
Bornat, Richard, Parkinson, Matthew, O'Hearn, Peter
This paper contains a model and a proof of soundness for a range of program logics based on separation logic and including the notions of permission and ownership for stack variables. It shows that...
Variables as resource in Hoare logic. (2006)
Bornat, Richard, Calcagno, Cristiano, Parkinson, Matthew
This paper contains a model and a proof of soundness for a range of program logics based on separation logic and including the notions of permission and ownership for stack variables. It shows that...
Variables as resource in Hoare logic. (2006)
Bornat, Richard, Calcagno, Cristiano, Parkinson, Matthew
This paper contains a model and a proof of soundness for a range of program logics based on separation logic and including the notions of permission and ownership for stack variables. It shows that...
Variables as resources in separation logic. (2006)
Bornat, Richard, Calcagno, Cristiano, Yang, Hongseok
This paper applied the separation logic notions of ownership and permission to ‘stack' variables that made it possible to banish the variable-use side conditions (e.g. on concurrency and frame...
Variables as resources in separation logic. (2006)
Bornat, Richard, Calcagno, Cristiano, Yang, Hongseok
This paper applied the separation logic notions of ownership and permission to ‘stack' variables that made it possible to banish the variable-use side conditions (e.g. on concurrency and frame...
The camel has two humps (working title) (2006)
Learning to program is notoriously difficult. A substantial minority of students fails in every introductory programming course in every UK university. Despite heroic academic effort, the proportion...
The camel has two humps (working title) (2006)
Learning to program is notoriously difficult. A substantial minority of students fails in every introductory programming course in every UK university. Despite great academic effort, the proportion...
Variables as Resource in Hoare Logics (2006)
Matthew Parkinson And, Matthew Parkinson, Richard Bornat
Hoare logic is bedevilled by complex but coarse side conditions on the use of variables. We define a logic, free of side conditions, which permits more precise statements of a program's use of...
Variables as resource in Hoare logics (2006)
Matthew Parkinson, Richard Bornat
Hoare logic is bedevilled by complex but coarse side conditions on the use of variables. We define a logic, free of side conditions, which permits more precise statements of a program’s use of...
Variables as resource in Hoare logics (2006)
Matthew Parkinson, Richard Bornat, Cristiano Calcagno
Hoare logic is bedevilled by complex and unmemorable side conditions on the use of variables. We define a logic free of side conditions, and show that it admits translations of proofs in Hoare logic,...
Permission accounting in separation logic. (2005)
Bornat, Richard, Calcagno, Cristiano, Parkinson, Matthew, O'Hearn, Peter
Concurrent separation logic includes the notion of ‘ownership' of a heap data structure that can be transferred between processes. This paper refined that idea with permission – partial ownership...
Permission accounting in separation logic. (2005)
Bornat, Richard, Calcagno, Cristiano, Parkinson, Matthew, O'Hearn, Peter
Concurrent separation logic includes the notion of ‘ownership' of a heap data structure that can be transferred between processes. This paper refined that idea with permission – partial ownership...
Permission Accounting in Separation Logic (2005)
Richard Bornat School, Richard Bornat, Cristiano Calcagno, Matthew Parkinson
A lightweight logical approach to race-free sharing of heap storage between concurrent threads is described, based on the notion of permission to access. Transfer of permission between threads,...
Local Reasoning, Separation and Aliasing (2004)
Richard Bornat School, Richard Bornat
Structures built by pointer aliasing, such as DAGs and graphs, are notoriously tricky to deal with. The mechanisms of separation logic can deal with these structures, but so far this has been done by...
Aczel, James, Fung, Pat, Bornat, Richard, Oliver, Martin, O'Shea, Tim, Sufrin, Bernard
This paper describes a research project into undergraduates’ use of a software tool to learn symbolic logic—a complex abstract domain that has been shown to be intimidating for students. The...
Program logic and equivalence in the presence of garbage collection (2003)
Cristiano Calcagno, Richard Bornat
It is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over memory....
Program logic and equivalence in the presence of garbage collection (2003)
Cristiano Calcagno, Richard Bornat
Abstract. It is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over...
Program logic and equivalence in the presence of garbage collection (2003)
Cristiano Calcagno, Richard Bornat
Abstract. Garbage collection relieves the programmer of the burden of managing dynamically allocated memory, by providing an automatic way to reclaim unneeded storage. It is generally thought that...
Program logic and equivalence in the presence of garbage collection (2001)
Cristiano Calcagno, Richard Bornat
Abstract. It is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over...
Proving pointer programs in Hoare Logic (2000)
. It is possible, but difficult, to reason in Hoare logic about programs which address and modify data structures defined by pointers. The challenge is to approach the simplicity of Hoare...
Using computers to learn logic: undergraduates' experiences (1999)
Aczel, James, Fung, P., Bornat, Richard, Oliver, Martin, O'Shea, Tim, Sufrin, Bernard
Learning formal logic can be difficult for many students. This paper describes some ongoing research into a computer program designed to help computer science undergraduates learn the natural...
Using computers to learn logic: undergraduates' experiences (1999)
Aczel, James, Fung, P., Bornat, Richard, Oliver, Martin, O'Shea, Tim, Sufrin, Bernard
Learning formal logic can be difficult for many students. This paper describes some ongoing research into a computer program designed to help computer science undergraduates learn the natural...
User Interfaces for Generic Proof Assistants Part I: Interpreting Gestures (1998)
Bernard Sufrin, Richard Bornat
JAPE is a generic proof editor which (amongst other things) offers the teacher, user, or logic designer the opportunity of constructing a direct manipulation interface for proofs. In part I of this...
Richard Bornat, Bernard Sufrin
Jape is a proof editor designed for use by novices and to be programmed by tyro logicians. Its user interface intrudes as little as possible into the business of making and writing down a proof; its...
The Calculator Project - Formal Reasoning about Programs (1995)
Steve Reeves, Doug Goldson, Pat Fung, Mike Hopkins, Richard Bornat
This paper describes The Calculator Project, which was a three-year joint research project between the Centre for Information Technology in Education at The Open University, U.K. (Pat Fung, Tim...
The Vectorisation Monad (1994)
Keith M. Clarke, Richard Bornat
: Traditionally a vectorising compiler matches the iterative constructs of a program against a set of predefined templates. If a loop contains no dependency cycles then a map template can be used;...
User Interfaces for Generic Proof Assistants Part II: Displaying Proofs
Bernard Sufrin Richard, Richard Bornat
JAPE is a generic proof editor which (amongst other things) offers the teacher, user, or logic designer the opportunity of constructing a direct manipulation interface for proofs. In the first part...
Richard Bornat, Bernard Sufrin
IONAA) IS FROMX=YANDAA(Y) INFER AA(X) 1 The ABSTRACTION annotation directs Jape to interpret the juxtaposition formulæ AA(Y) and AA(X) as shorthand for substitution forms. The parameter X allows us...