Publications
102 results found
Aublin P-L, Kelbert F, O'Keffe D, et al., 2018, LibSEAL: revealing service integrity violations using trusted execution, Departmental Technical Report: 18/2, Publisher: Department of Computing, Imperial College London
Users of online services such as messaging, code hosting and collaborativedocument editing expect the services to uphold the integrityof their data. Despite providers’ best efforts, data corruption stilloccurs, but at present service integrity violations are excluded fromSLAs. For providers to include such violations as part of SLAs, thecompeting requirements of clients and providers must be satisfied.Clients need the ability to independently identify and prove serviceintegrity violations to claim compensation. At the same time,providers must be able to refute spurious claims.We describe LibSEAL, a SEcure Audit Library for Internet servicesthat creates a non-repudiable audit log of service operationsand checks invariants to discover violations of service integrity.LibSEAL is a drop-in replacement for TLS libraries used by services,and thus observes and logs all service requests and responses. It runsinside a trusted execution environment, such as Intel SGX, to protectthe integrity of the audit log. Logs are stored using an embeddedrelational database, permitting service invariant violations to bediscovered using simple SQL queries. We evaluate LibSEAL withthree popular online services (Git, ownCloud and Dropbox) anddemonstrate that it is effective in discovering integrity violations,while reducing throughput by at most 14%.
Department of Computing, Imperial College London, 2016, High volume ergonomic simulation of chairs, Departmental Technical Report: 16/4, Publisher: Department of Computing, Imperial College London, 16/4
To understand what makes a chair comfortable or practical we need to test a largenumber of chairs, both good and bad. Due to the numbers involved we cannot achievethis with physical testing. Instead we use simpli ed ergonomic simulations. The sim-ulations presented here produce pressure maps within the range given the literature,along with several other measures of comfort and practicality. This was done sub-stantially faster than examples in the literature, permitting collection of thousands ofresults.
Cogumbreiro T, Hu R, Martins F, et al., 2014, Dynamic deadlock verification for general barrier synchronisation, Departmental Technical Report: 14/12, Publisher: Department of Computing, Imperial College London, 14/12
We present Armus, a dynamic verification tool for deadlock detectionand avoidance specialised in barrier synchronisation. Barriersare used to coordinate the execution of groups of tasks, and serve asa building block of parallel computing. Our tool verifies more barriersynchronisation patterns than current state-of-the-art. To improvethe scalability of verification, we introduce a novel eventbasedrepresentation of concurrency constraints, and a graph-basedtechnique for deadlock analysis. The implementation is distributedand fault-tolerant, and can verify X10 and Java programs.To formalise the notion of barrier deadlock, we introduce a corelanguage expressive enough to represent the three most widespreadbarrier synchronisation patterns: group, split-phase, and dynamicmembership. We propose a graph analysis technique that selectsfrom two alternative graph representations: the Wait-For Graph,that favours programs with more tasks than barriers; and the StateGraph, optimised for programs with more barriers than tasks. Weprove that finding a deadlock in either representation is equivalent,and that the verification algorithm is sound and complete withrespect to the notion of deadlock in our core language.Armus is evaluated with three benchmark suites in local anddistributed scenarios. The benchmarks show that graph analysiswith automatic graph-representation selection can record a 7-foldexecution increase versus the traditional fixed graph representation.The performance measurements for distributed deadlock detectionbetween 64 processes show negligible overheads.
Jones AV, 2011, Imperial College Computing Student Workshop, Departmental Technical Report: 11/9, Publisher: Department of Computing, Imperial College London, 11/9
Sun K, Larminie C, Przulj N, 2011, Disease re-classi cation via integration of biological networks, Departmental Technical Report: 11/8, Publisher: Department of Computing, Imperial College London, 11/8
Currently, human diseases are classi ed as they were in the late 19th century, by consideringonly symptoms of the a ected organ. With a growing body of transcriptomic,proteomic, metabolomic and genomics data sets describing diseases, we ask whether theold classi cation still holds in the light of modern biological data. These large-scale andcomplex biological data can be viewed as networks of inter-connected elements.We propose to rede ne human disease classi cation by considering diseases as systemsleveldisorders of the entire cellular system. To do this, we will integrate di erenttypes of biological data mentioned above. A network-based mathematical model will bedesigned to represent these integrated data, and computational algorithms and tools willbe developed and implemented for its analysis. In this report, a review of the researchprogress so far will be presented, including 1) a detailed statement of the researchproblem, 2) a literature survey on relative research topics, 3) reports of on-going work,and 4) future research plans.2
Department of Computing, Imperial College London, 2011, Relationship-based access control: its expression and enforcement through hybrid logic, Departmental Technical Report: 11/12, Publisher: Department of Computing, Imperial College London, 11/12
Access control policy is typically de ned in terms of attributes,but in many applications it is more natural to de- ne permissions in terms of relationships that resources, systems,and contexts may enjoy. The paradigm of relationshipbasedaccess control has been proposed to address this issue,and modal logic has been used as a technical foundation.We argue here that hybrid logic { a natural and wellestablishedextension of modal logic { addresses limitationsin the ability of modal logic to express certain relationships.Also, hybrid logic has advantages in the ability to e cientlycompute policy decisions relative to a relationship graph.We identify a fragment of hybrid logic to be used forexpressing relationship-based access-control policies, showthat this fragment supports important policy idioms, andstudy its expressiveness. We also capture the previouslystudied notion of relational policies in a static type system.Finally, we point out that use of our hybrid logic removesan exponential penalty in existing attempts of specifyingcomplex relationships such as \at least three friends".
Brotherston J, Gore R, 2011, Craig interpolation in displayable logics, Departmental Technical Report: 11/1, Publisher: Department of Computing, Imperial College London, 11/1
We give a general proof-theoretic method for establishingCraig interpolation for displayable logics, based upon an analysis of theindividual proof rules of their display calculi. Using this uniform method,we establish interpolation for a spectrum of display calculi differing intheir structural rules, including those for multiplicative linear logic, mul-tiplicative additive linear logic and ordinary classical logic.Our analysis at the level of proof rules also provides new insights into thereasons why interpolation fails, or seems likely to fail, in many substruc-tural logics. Specifically, we identify contraction as being particularlyproblematic for interpolation except in special circumstances.
Brotherston J, Kanovich M, 2010, Undecidability of propositional separation logic and its neighbours, Departmental Technical Report: 10/1, Publisher: Department of Computing, Imperial College London, 10/1
Separation logic has proven an adequate formalism for theanalysis of programs that manipulate memory (in the formof pointers, heaps, stacks, etc.). In this paper, we considerthe purely propositional fragment of separation logic, as wellas a number of closely related substructural logical systems.We show that, surprisingly, all of these propositional logicsare undecidable. In particular, we solve an open problem byestablishing the undecidability of Boolean BI.
Bejleri A, 2010, Session typed parameterised communication patterns, Departmental Technical Report: 10/7, Publisher: Department of Computing, Imperial College London, 10/7
Communication patterns describe simple and elegant structured interactionsin communication based applications. They are used in many parallel computing architecturesof parallel algorithms, data exchange protocols and web-services. Communicationpatterns help programmers to design more efficient, structured, modular andunderstandable architectures, but they do not provide any automatic code validation.We study this problem using global session types, a type theory that describes structuredinteractions from a global point of view. We then augment the syntax of global typeswith parameters that abstract the number of participants and an iterative construct thatbuilds instances of parameterised communication patterns. Our formal system allowsprogrammers to represent parameterised communication patterns by global types andthen validate the code by type-checking.
Seng SP, Palem KV, Rabbah RM, et al., 2009, PDXML: extensible markup language for processor description, Departmental Technical Report: 02/16, Publisher: Department of Computing, Imperial College London, 02/16
This paper introduces PD-XML, a meta-language for describinginstruction processors in general and with an emphasison embedded processors, with the specific aim ofenabling their rapid prototyping, evaluation and eventualdesign and implementation. The proposed methodology isbased on the extensible markup language XML widely usedstructured information exchange and collaboration. PDXMLallows for both high-level and low-level architecturalspecifications required to support a toolchain for design spaceexploration. PD-XML consists of three intuitive entities,describing: (a) the storage components available in a design,(b) the instructions supported by an architecture, and(c) the resources afforded by the microarchitecture implementation.PD-XML is not specific to any one architecture,compiler or simulation environment and hence providesgreater flexibility than related machine description methodologies.We demonstrate how PD-XML can be interfaced toto existing description methodologies and tool-flows. In particular,we show how PD-XML specifications can be translatedinto appropriate machine descriptions for the parametricHPL-PD VLIW processor and for the flexible instructionprocessor approach.
Brotherston J, 2009, A cut-free proof theory for boolean BI (via display logic), Departmental Technical Report: 09/13, Publisher: Department of Computing, Imperial College London, 09/13
We give a display calculus proof system for Boolean BI (BBI) basedon Belnap’s general display logic. We show that cut-elimination holds inour system and that it is sound and complete with respect to the usualnotion of validity for BBI. We then show how to constrain proof searchin the system (without loss of generality) by means of a series of prooftransformations. By doing so, we gain some insight into the problem ofdecidability for BBI.
Thornley DJ, James JR, 2009, Defining and estimating value to a mission, Departmental Technical Report: 09/12, Publisher: Department of Computing, Imperial College London, 09/12
Selection of assignments for a constrainedinventory of assets and associated services requires comparablemeasures of their value to the potential recipients, and anyassociated costs. The dissemination of information or intelligenceproducts over bandwidth limited and security constrainedchannels similarly requires consideration of the associated valuesand costs. Similar reasoning is applicable to the selection ofvariant effects and methods. We present an approach to valuedefinition and prediction in the mission performancecharacteristics resulting from variant deployments.
Thornley DJ, Harvey MP, 2009, A first cut of the military QoI attribute space and hypothesis structure for abductive reasoning, Departmental Technical Report: 09/11, Publisher: Department of Computing, Imperial College London, 09/11
The concept of quality of information (QoI)provides a focus for developing and evaluating informationgathering and situational awareness (SA) assessment methods.Effective prima facie estimates of accuracy, latency andtrustworthiness are essential elements in the assessment of aninformation product delivered to, for example, a decision makercharged with timely and accurate identification of targets. QoImust support reasoning under conditions of uncertainty andconflict, which is a motivation for the application of abductivereasoning. This type of reasoning evokes hypotheses for groundtruth that include the characteristics of the subject matter,contexts, producers and channels of information products. Forour purposes, hypotheses are to be tested using a model related inintent to the enterprise QoI space of Wang et al, but which musttake into consideration a significantly richer set of uncertaintiesresulting from the complexity and range of military activitiesthat may require concurrent evaluation. This paper andaccompanying poster begin to define that space.
Thornley D, Young R, Richardson J, 2009, Development of a Mission Abstraction Requirements Structure (MARS) and stochastic modelling for sensing service-driven mission performance prediction, Departmental Technical Report: 09/10, Publisher: Department of Computing, Imperial College London, 09/10
Spacey SA, 2009, Concise cplex, Departmental Technical Report: 09/7, Publisher: Department of Computing, Imperial College London, 09/7
This paper is a concise guide to CPLEX, the leading solverfor linear and convex quadratic optimisation problems. Thepaper is self contained and includes information for firsttime CPLEX users as well as code snippets and lemmas thatmay be of referential value to experienced users.The paper starts with a brief explanation of how to runCPLEX on departmental servers at Imperial and on standalonemachines in section 1, how to create and solve simpleLinear Programs in section 2 and how to obtain detailed solutionresults in section 3. The paper then moves on to discussseveral CPLEX issues and quirks that may confuse firsttime users including: anomalous objective values causedby big-M scaling, the implications of long MILP solutiontimes and removing memory limitations for problems withlarge MILP solution trees. The paper concludes with logicalequivalence proofs in section 9 that can be used as a startingpoint for complex problem translation and references areprovided for additional reading.
Cardelli L, Gardner P, 2009, Processes in space, Departmental Technical Report: 09/4, Publisher: Department of Computing, Imperial College London, 09/4
We introduce a geometric process algebra based on affine geometry,with the aim of describing the concurrent evolution of geometric structures in3D space. We prove a relativity theorem stating that algebraic equations are invariantunder rigid body transformations.
Nickovic D, Piterman N, 2009, From MTL to deterministic timed automata, Departmental Technical Report: 09/2, Publisher: Department of Computing, Imperial College London, 09/2
In this paper we propose a novel technique for constructing timed automatafrom properties expressed in the logic MTL, under bounded-variabilityassumptions. We handle full MTL and in particular do not impose bounds on thefuture temporal connectives. Our construction is based on separation of the continuoustime monitoring of the input sequence and discrete predictions regardingthe future. The separation of the continuous from the discrete allows us to furtherdeterminize our automata. This leads, for the first time, to a construction fromfull MTL to deterministic timed automata.
Katwala-Argent A, Dingle N, Harder U, 2008, 24th UK performance engineering workshop, Departmental Technical Report: 08/9, Publisher: Department of Computing, Imperial College London, 08/9
Departmental Technical Report: 08/9
Schroder L, Pattinson D, 2008, The craft of model making: PSPACE bounds for non-iterative modal logics, Departmental Technical Report: 08/3, Department of Computing, Imperial College London, Publisher: Department of Computing, Imperial College London, 08/3
The methods used to establish PSPACE-bounds for modal logics can roughly be groupedinto two classes: syntax driven methods establish that exhaustive proof search can beperformed in polynomial space whereas semantic approaches directly construct shallowmodels. In this paper, we follow the latter approach and establish generic PSPACE-bounds for a large and heterogeneous class of modal logics in a coalgebraic framework.In particular, no complete axiomatisation of the logic under scrutiny is needed. Thisdoes not only complement our earlier, syntactic, approach conceptually, but also coversa wide variety of new examples which are di cult to harness by purely syntactic means.Apart from re-proving known complexity bounds for a large variety of structurally di erentlogics, we apply our method to obtain previously unknown PSPACE-bounds for Elgesem'slogic of agency and for graded modal logic over reexive frames.
Matt P-A, Toni F, 2008, A game-theoretic perspective on the notion of argument strength in abstract argumentation, Departmental Technical Report: 08/11, Publisher: Department of Computing, Imperial College London, 08/11
This paper is concerned with the problem of quantifying the strengthof arguments in controversial debates, which we model as abstract argumentationframeworks [Dung, 1995]. Standard approaches to abstract argumentation provideonly a qualitative account of the status of arguments, whereas numerical measuresof argument strength might provide a more precise evaluation of their individualstatus. Intuitively, the strength of an argument in a debate essentially depends onhow a proponent of that argument would defend himself against the criticisms ofsomeone opposed to the argument. Since there can be many ways of defending andattacking an opinion, we essentially conceive argument strength as an equilibriumresulting from the interactions taking place between the opinions that a proponentand an opponent of the argument could a priori embrace. More formally, we defineargument strength in terms of the value of a repeated two-person zero-sum strategicgame with imperfect information. Then, using the game-theoretic properties ofsuch games and notably the von Neumann minimax theorem [Neumann, 1928], weestablish and illustrate the main properties of this new argument strength measure.
Pattinson D, Shroder L, 2008, Cut elimination in coalgebraic logics, Departmental Technical Report: 08/14, Publisher: Department of Computing, Imperial College London, 08/14
We give two generic proofs for cut elimination in propositional modallogics, interpreted over coalgebras. We first investigate semantic coherenceconditions between the axiomatisation of a particular logic andits coalgebraic semantics that guarantee that the cut-rule is admissiblein the ensuing sequent calculus. We then independently isolate apurely syntactic property of the set of modal rules that guarantees cutelimination. Apart from the fact that cut elimination holds, our mainresult is that the syntactic and semantic assumptions are equivalent incase the logic is amenable to coalgebraic semantics. As applicationswe present a new proof of the (already known) interpolation propertyfor coalition logic and newly establish the interpolation property forthe conditional logics CK and CK + ID.
Wu Q, Mencer O, Tavares C, et al., 2008, Hotspot detection of SPEC CPU 2006 benchmarks with performance event counters, Departmental Technical Report: 08/8, Publisher: Department of Computing, Imperial College London, 08/8
Hotspot is the part of a program where most execution timeis spent. Detecting the hotspot enables the optimization of the program.The performance event counters embedded in modern processors providethe hardware support for the hotspot detection. By sampling the instruc-tion addresses of the running program with performance event counters,hotspot of the program can be statistically detected. This technical re-port describes our tool to find the sections of the code that are detectedas the hotspot of the program with performance event counters. SPECCPU 2006 benchmarks are tested with our tool and the results show thehotspot sections and overhead of the hotspot detection tool.
Spacey SA, 2008, 3S: program instrumentation and characterisation framework, Departmental Technical Report: 08/1, Publisher: Department of Computing, Imperial College London, 08/1
3S is an efficient program instrumentation and profilingframework. 3S is only 288 lines of framework code, yet itcan produce the same reports as Valgrind [1] and is up to anorder of magnitude faster.
Hussain A, Toni F, 2008, On the benefits of argumentation for negotiation - preliminary version, Departmental Technical Report: 08/15, Publisher: Department of Computing, Imperial College London, 08/15
We present preliminary work on the benefits of argumentation-basednegotiation, for a simple framework for one-to-one negotiation betweenagents in a resource reallocation setting. Agents engage in dialogues withother agents in order to obtain resources they need but do not have. Di-alogues are regulated by simple communication policies that allow agentsto provide reasons (arguments) for their refusals to give away resources;agents use assumption-based argumentation in order to deploy these poli-cies. We assess the benefits of providing these reasons both informallyand experimentally: by providing reasons, agents are “more effective”in identifying a reallocation of resources if one exists and failing if noneexists.
Matt P-A, Toni F, 2008, Constructing imprecise probabilities using arguments as evidence, Departmental Technical Report: 08/10, Publisher: Department of Computing, Imperial College London, 08/10
This paper addresses the problem of constructing subjective impreciseprobabilities using qualitative and conflicting pieces of information (arguments) asevidence.We propose formulae for the calculus of imprecise probabilities and showthat the probabilities obtained reflect the indeterminacy of the subject, faithfullyquantify the support offered by the arguments and constitute previsions that aremathematically coherent in the sense of [Walley, 1991].
Bradley JT, 2007, RCAT: from PEPA to product form, Departmental Technical Report: 07/2, Publisher: Department of Computing, Imperial College London, 07/2
Schroder L, Pattinson D, 2007, PSPACE bounds for Rank-1 modal logics, Departmental Technical Report: 07/4, Publisher: Department of Computing, Imperial College London, 07/4
For lack of general algorithmic methods that apply to wide classes of logics, establishing a com-plexity bound for a given modal logic is often a laborious task. The present work is a step towardsa general theory of the complexity of modal logics. Our main result is that all rank-1 logics enjoya shallow model property and thus are, under mild assumptions on the format of their axioma-tisation, in PSPACE. This leads to a unified derivation of tight PSPACE-bounds for a numberof logics including K, KD, coalition logic, graded modal logic, majority logic, and probabilisticmodal logic. Our generic algorithm moreover finds tableau proofs that witness pleasant proof-theoretic properties including a weak subformula property. This generality is made possible by acoalgebraic semantics, which conveniently abstracts from the details of a given model class andthus allows covering a broad range of logics in a uniform way.
Ruuth S, Maros I, Nieminen K, 2007, A multiobjective dynamic nonlinear robot assignment problem, Departmental Technical Report: 07/3, Publisher: Department of Computing, Imperial College London, 07/3
Robots will be used under rapidly changing and highly dangerous circumstancessuch as rescue operations in a radioactive environment or a fire as well as militaryoperations. The robots are sent to several targets in order to carry out varioustasks.The robots we are considering here are able to send and receive messages toand from each other as well as solve nonlinear assignment problems. When therobot salvo is en-route to their targets several events may happen. A number of co-operative robots may get jammed as a consequence of disturbances. Some robotsmay already have reached their targets. Some robots may not be able to reachall targets. The system being investigated enables the surviving robots to worktogether in real time and change their pre-set tasks if necessary in order to maximizetheir effectiveness. In this paper we present a method which solves the reallocationproblem using a piecewise linear network algorithm. Experimental results up to 493targets and 500 robots show that the reallocation of the robots can be done in realtime.
Ezechukwu O, Maros I, 2007, A genetic algorithm for automated model formulation, Departmental Technical Report: 07/1, Publisher: Department of Computing, Imperial College London, 07/1
The challenge of automating the formulation of optimization models is to produce,from a problem description, a well-formed model, which is a mathematically accuraterepresentation of the real-world decision-making problem being considered, andwhich is suitable for computational purposes. This can be stated more formally as theautomation problem, which is the problem of providing intelligent (i.e. automated)assistance during the formulation stage of the mathematical programming process. Inthis paper, we explore the need to automate model formulation, thus providing abackground on the automation problem. We also detail a solution to the problemwhich is based on evolutionary search techniques.
Pitt J, Kamara L, Sergot M, et al., 2006, Voting in multi-agent systems, COMPUTER JOURNAL, Vol: 49, Pages: 156-170, ISSN: 0010-4620
- Author Web Link
- Cite
- Citations: 37
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.