Browsing by Author "BUTTERFIELD, ANDREW"
Now showing items 1-13 of 13
-
Concurrent Models of Flash Memory Device Behaviour
BUTTERFIELD, ANDREW (Springer, 2009)We present a CSP model of the internal behaviour of Flash Memory, based on its specification by the Open Nand-Flash Interface (ONFi) consortium. This contributes directly to the low-level modelling of the data-storage ... -
The Denotational Semantics of Slotted-Circus
BUTTERFIELD, ANDREW (Springer, 2009) -
A Feature Model of Actor, Agent, Functional, Object, and Procedural Programming Languages
BUTTERFIELD, ANDREW (2015)The number of programming languages is large [1] and steadily increasing [2]. However, little structured information and empirical evidence is available to help software engineers assess the suitability of a language for ... -
Mechanising a Formal Model of Flash Memory
BUTTERFIELD, ANDREW (Elsevier, 2009)We present second steps in the construction of formal models of NAND flash memory, based on a recently emerged open standard for such devices. The model is intended as a key part of a pilot project to develop a verified ... -
Modelling the Haemodialysis Machine with Circus
BUTTERFIELD, ANDREW (Springer International Publishing, 2016) -
POSIX and the verification grand challenge: A roadmap
BUTTERFIELD, ANDREW (IEEE, 2008) -
Saoithín: A Theorem Prover for UTP
BUTTERFIELD, ANDREW (Springer, 2010)Saoithín 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 ... -
Separation Kernel Verification: The XtratuM Case Study
BUTTERFIELD, ANDREW (Springer, 2014) -
Towards a UTP-style framework to deal with probabilities
BUTTERFIELD, ANDREW; BRESCIANI, RICCARDO (TCD-CS Technical Reports, 2011)We present an encoding of the semantics of the probabilistic guarded command language (pGCL) in the Unifying Theories of Programming (UTP) framework. Our contribution is a UTP encoding that captures pGCL programs as ... -
UTCP: compositional semantics for shared-variable concurrency
BUTTERFIELD, ANDREW (Springer, 2017) -
UTP Semantics for Shared-State, Concurrent, Context-Sensitive Process Models
BUTTERFIELD, ANDREW (IEEE Computer Society, 2016) -
UTP2: Higher-Order Equational Reasoning by Pointing
BUTTERFIELD, ANDREW (2014)We describe a prototype theorem prover, U.(TP)2, developed to match the style of hand-written proof work in the Unifying Theories of Programming semantical framework. This is based on alphabetised predicates in a 2nd-order ... -
UTPCalc - A calculator for UTP Predicates
BUTTERFIELD, ANDREW (Springer International Publishing, 2017)