ISSN 1476-2986TCP, UDP, and Sockets: Volume 3: The Service-level Specification (2009)
Thomas Ridge, Michael Norrish, Peter Sewell, Thomas Ridge, Michael Norrish, Peter Sewell
Despite more than 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code. In part...
TCP, UDP, and Sockets: Volume 3: The Service-level Specification (2009)
Thomas Ridge, Michael Norrish, Peter Sewell
Despite more than 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code. In part...
A rigorous approach to networking: TCP, from implementation to protocol to service (2009)
Tom Ridge, Michael Norrish, Peter Sewell
Abstract. Despite more then 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code....
The Design of Distributed Programming Languages (2008)
Peter Sewell, John Billings, Steve Bishop, Matthew Fairbairn, Pierre Habouzit, Michael Hicks, ...
High-level programming languages For non-distributed, non-concurrent programming, they’re pretty good. We have ML (SML/OCaml), Haskell, Java, C#, with: • type safety • rich concrete types –...
A rigorous approach to networking: TCP (2008)
from implementation to protocol to service
A rigorous approach to networking: TCP (2008)
Tom Ridge, Michael Norrish, Peter Sewell
from implementation to protocol to service
A rigorous approach to networking: TCP, from implementation to protocol to service (2008)
Tom Ridge, Michael Norrish, Peter Sewell
Abstract. Despite more then 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code....
A thread of HOL development (2008)
The HOL system is a mechanized proof assistant for higher order logic that has been under continuous development since the mid-1980s, by an ever-changing group of developers and external...
Proof Pearl: de Bruijn Terms Really Do Work (2008)
Michael Norrish, René Vestergaard
Abstract. Placing our result in a web of related mechanised results, we give a direct proof that the de Bruijn λ-calculus (à la Huet, Nipkow and Shankar) is isomorphic to an α-quotiented...
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof (2008)
Abstract. We discuss methods for dealing effectively with let-bindings in proofs. Our contribution is a small set of unconditional rewrite rules, found by the bracket abstraction translation from the...
Acute and TCP: specifying and developing abstractions for global computation (2008)
James Leifer, Michael Norrish, Peter Sewell, Keith Wansbrough
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
The TCP/IP protocols and Sockets API underlie much of modern computation, but their semantics have historically been very complex and ill-defined. The real standard is the de facto one of the common...
A rigorous approach to networking: TCP, from implementation to protocol to service (2008)
Tom Ridge, Michael Norrish, Peter Sewell
Abstract. Despite more then 30 years of research on protocol specification, the major protocols deployed in the Internet, such as TCP, are described only in informal prose RFCs and executable code....
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
The TCP/IP protocols and Sockets API underlie much of modern computation, but their semantics have historically been very complex and ill-defined. The real standard is the de facto one of the common...
A rigorous approach to networking: TCP (2008)
Tom Ridge, Michael Norrish, Peter Sewell
from implementation to protocol to service
Engineering with Logic: HOL Specification and (2008)
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, ...
The TCP/IP protocols and Sockets API underlie much of modern computation, but their semantics have historically been very complex and ill-defined. The real standard is the de facto one of the common...
Workshop Program 5th International Verification Workshop – VERIFY’08 (2008)
Bernhard Beckert, Gerwin Klein (chairs, Bernhard Beckert, Bernhard Beckert, Gerwin Klein, ...
The VERIFY workshop series aims at bringing together people who are interested in the development of safety and security critical systems, in formal methods, in the development of automated theorem...
A Tool for Implementing Action Graphs (2007)
Philippa Gardner, Michael Norrish
Milner introduced the action calculus framework as a graphical framework for describing many models of interactive behaviour. We describe a specification tool for action graphs, which allows the user...
PEer-toPeer Implementation and TheOry Workpackage 1: Formal Models (2007)
Peter Sewell, Keith Wansbrough, Steven Bishop, Michael Norrish, Ucam The
We discuss each in turn, concluding by listing the associated papers published during this year. 1 Transactions and the Semantics of Failure Overview Work in this task has proceeded at three levels...
of Church's formulation of Simple Type Theory (2007)
The HOL system is a mechanized proof assistant for higher order logic that has been under continuous development since the mid-1980s, by an ever-changing group of developers and external...
Timing UDP:MechanizedSemantics forSockets,Threads, andFailures (2007)
Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov
www.cl.cam.ac.uk/users/pes20/Netsem Abstract. This paper studies the semantics of failure in distributed programming. We present a semantic model for distributed programs that use the standard...
Technical Report Number 453 C formalised in HOL (2007)
We present a formal semantics of the C programming language, covering both the type system and the dynamic behaviour of programs. The semantics is wide-ranging, covering most of the language, with...
Michael Norrish, Peter Sewell, Keith Wansbrough
is good for you and feasible: reflections on formal treatments of
PROSPER: LTR 26241 The PROSPER Toolkit (2007)
Graham Collins, L. Dennis, G. Collins, M. Norrish, The Prosper Toolkit, Louise Dennis, ...
1 The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they...
A tool for implementing action graphs (2007)
Michael Norrish, Andrei Serjantov
We describe a specification tool for action graphs, which allows the user to naturally switch between between the syntactic and graphical presentations. The implementation includes a general matching...
PEer-toPeer Implementation and TheOry Workpackage 1: Formal Models (2007)
Peter Sewell, Keith Wansbrough, Steven Bishop, Michael Norrish, Ucam The
We discuss each in turn, concluding by listing the associated papers published during this year. 1 Transactions and the Semantics of Failure Overview Work in this task has proceeded at three levels...
Barendregt’s variable convention in rule inductions (2007)
Christian Urban, Stefan Berghofer, Michael Norrish
Abstract. Inductive definitions and rule inductions are two fundamental reasoning tools in logic and computer science. When inductive definitions involve binders, then Barendregt's variable...
Barendregt’s variable convention in rule inductions (2007)
Christian Urban, Stefan Berghofer, Michael Norrish
Abstract. Inductive definitions and rule inductions are two fundamental reasoning tools in logic and computer science. When inductive definitions involve binders, then Barendregt’s variable...
Barendregt’s variable convention in rule inductions (2007)
Christian Urban, Stefan Berghofer, Michael Norrish
Abstract. Inductive definitions and rule inductions are two fundamental reasoning tools in logic and computer science. When inductive definitions involve binders, then Barendregt’s variable...
W. Ahrendt, P. Baumgartner, H. De Nivelle, Johan Bos, Simon Colton, Christian Fermüller, ...
Our field is called automated theorem proving because traditionally it has been concerned with the art of finding proofs automatically. In the beginning, researchers were motivated by the wish to...
Rigorous Specification and Conformance Testing (2005)
Techniques For Network, Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, ...
Network protocols are hard to implement correctly. Despite the existence of RFCs and other standards, implementations often have subtle differences and bugs. One reason for this is that the...
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
We have developed a mathematically rigorous and experimentally-validated post-hoc specification of the behaviour of TCP, UDP, and the Sockets API. It characterises the API and network-interface...
Rigorous And Experimentally-Validated, Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, ...
We have developed a mathematically rigorous and experimentally-validated post-hoc specification of the behaviour of TCP, UDP, and the Sockets API. It characterises the API and network-interface...
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
Network protocols are hard to implement correctly. Despite the existence of RFCs and other standards, implementations often have subtle differences and bugs. One reason for this is that the...
rigorous and experimentally-validated behavioural specification Volume 1: Overview (2005)
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough, ...
rigorous and experimentally-validated behavioural specification
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
Network protocols are hard to implement correctly. Despite the existence of RFCs and other standards, implementations often have subtle differences and bugs. One reason for this is that the...
Recursive function definition for types with binders (2004)
Abstract. This work describes the proof and uses of a theorem allowing definition of recursive functions over the type of λ-calculus terms, where terms with bound variables are identified up to...
Complete integer decision procedures as derived rules in HOL (2003)
Abstract. I describe the implementation of two complete decision procedures for integer Presburger arithmetic in the HOL theorem-proving system. The first procedure is Cooper’s algorithm, the...
Rigour is Good for You and Feasible: (2002)
Reflections On Formal, Michael Norrish, Peter Sewell, Keith Wansbrough
Introduction We summarise two projects that formalised complex real world systems: UDP and its sockets API, and the C programming language. We describe their goals and the techniques used in both. We...
Timing UDP: mechanized semantics for sockets, threads and failures (2002)
Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov
www.cl.cam.ac.uk/users/pes20/Netsem Abstract. This paper studies the semantics of failure in distributed programming. We present a semantic model for distributed programs that use the standard...
Rigour is good for you and feasible: reflections on formal treatments of C and UDP sockets (2002)
Michael Norrish, Peter Sewell, Keith Wansbrough
Introduction We summarise two projects that formalised complex real world systems. We describe their goals and the techniques used in both. We conclude by discussing how such techniques might be...
Timing UDP: mechanized semantics for sockets, threads and failures (2002)
Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov
This paper studies the semantics of failure in distributed programming. We present a semantic model for distributed programs that use the standard sockets interface; it covers message loss, host...
A Thread of HOL Development (2002)
Norrish, Michael, Slind, Konrad
The HOL system is a mechanized proof assistant for higher-order logic that has been under continuous development since the mid-1980s, by an ever-changing group of developers and external...
Dennis, Louise Abigail, Collins, Graham, Norrish, Michael, Boulton, Richard, Slind, Konrad, Robinson, Graham, ...
The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they...
Dennis, Louise Abigail, Collins, Graham, Norrish, Michael, Boulton, Richard, Slind, Konrad, Robinson, Graham, ...
The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they...
K. Slind, Louise Dennis, Louise Dennis, Michael Norrish, Michael Norrish, Konrad Slind, ...
The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they...
Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Graham Robinson, ...
The Prosper (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they...
Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Tom Melham
project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they may be treatedas components. A system incorporating such tools...
Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Tom Melham
project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they may be treatedas components. A system incorporating such tools...
Dennis, Louise Abigail, Collins, Graham, Norrish, Michael, Boulton, Richard, Slind, Konrad, Robinson, Graham, ...
The PROSPER (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they...
Deterministic expressions in C (1999)
Abstract. Expressions in the programming language C have such an under-specified semantics that one might expect them to be non-deterministic. However, with the help of a mechanised formalisation, we...
Deterministic expressions in C (1999)
. Expressions in the programming language C have such an under-specified semantics that one might expect them to be non-deterministic. However, with the help of a mechanised formalisation, we have...
We present a formal semantics of the C programming language, covering both the type system and the dynamic behaviour of programs. The semantics is wide-ranging, covering most of the language, with...
An abstract dynamic semantics for C (1997)
This report is a presentation of a formal semantics for the C programming language. The semantics has been defined operationally in a structured semantics style and covers the bulk of the core of the...
An abstract dynamic semantics for C (1997)
This report is a presentation of a formal semantics for the C programming language. The semantics has been defined operationally in a structured semantics style and covers the bulk of the core of the...
Derivation of verification rules for C from operational definitions (1996)
While a low-level, operational definition of a language's semantics is a straightforward way of specifying the behaviour of programs written in that language, it is not necessarily very suitable...