University of Limerick Institutional Repository

Browsing LERO - Project partner authors by Author "Butterfield, Andrew"

DSpace Repository

Browsing LERO - Project partner authors by Author "Butterfield, Andrew"

Sort by: Order: Results:

  • Bresciani, Riccardo; Butterfield, Andrew (IEEE Computer Society, 2009)
    When some agents want to communicate through a media stream (for example voice or video), the Real Time Protocol (RTP) is used. This protocol does not provide encryption, so it is necessary to use Secure RTP (SRTP) to ...
  • Bresciani, Riccardo; Butterfield, Andrew (Springer, 2013)
    We have introduced probability in the UTP framework by using functions from the state space to real numbers, which we term distributions, that are embedded in the predicates describing the di er- ent program constructs. ...
  • Butterfield, Andrew (2012)
    U (TP)2 is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higher-order logic, alphabets, equational reasoning and \programs as ...
  • Gomes, Arthur O; Butterfield, Andrew (Springer, 2016)
    We present a formal model of aspects of the haemodialysis machine case study using the Circus speci cation notation. We focus on building a model in which each of the software requirements (R-1{36) are represented by a ...
  • Bresciani, Riccardo; Butterfield, Andrew (2012)
    We present a theory of designs based on functions from the state space to real numbers, which we term distributions. This theory uses predicates, in the style of UTP, based on homogeneous relations between distributions, ...
  • Bresciani, Riccardo; Butterfield, Andrew (Springer, 2012)
    We present an encoding of the semantics of the probabilis- tic guarded command language (pGCL) in the Unifying Theories of Programming (UTP) framework. Our contribution is a UTP encoding that captures pGCL programs as ...
  • Butterfield, Andrew (Springer, 2016)
    We present the development of the UTP-Calculator: a tool, written in Haskell, that supports rapid prototyping of new theories in the Unifying Theories of Programming paradigm, by supporting an easy way to very quickly ...
  • Bresciani, Riccardo; Butterfield, Andrew (Association for Computing Machinery, 2009)
    The Dolev-Yao model has been widely used in protocol verificaion and has been implemented in many protocol verifiers. There are strong assumptions underlying this model, such as perfect cryptography: the aim of the ...

Search ULIR


Browse

My Account

Statistics