Theoretical Computer Science Group
Browse by
Recent Submissions
-
Trace Properties from Separation Logic Specifications
We propose a formal approach for relating abstract separation logic library specifications with the trace properties they enforce on interactions between a client and a library. Separation logic with abstract predicates ... -
Exploring Human Cognition Using Large Image Databases.
(2016-07)Most cognitive psychology experiments evaluate models of human cognition using a relatively small, well-controlled set of stimuli. This approach stands in contrast to current work in neuroscience, perception, and computer ... -
A Case Study of Controlling Crossover in a Selection Hyper-heuristic Framework Using the Multidimensional Knapsack Problem
(MIT Press, 2016-03)Hyper-heuristics are high-level methodologies for solving complex problems that operate on a search space of heuristics. In a selection hyper-heuristic framework, a heuristic is chosen from an existing set of low-level ... -
A Case Study of Controlling Crossover in a Selection Hyper-heuristic Framework Using the Multidimensional Knapsack Problem.
(2016)Hyper-heuristics are high-level methodologies for solving complex problems that operate on a search space of heuristics. In a selection hyper-heuristic framework, a heuristic is chosen from an existing set of low-level ... -
Modelling the User
We overview our research on the formal modelling of user behaviour, generic user modelling,, as a form of usability evaluation looking for design flaws that lead to systematic human error. This involves formalising principles ... -
Nominal Game Semantics.
(2016) -
smid: A Black-Box Program Driver
(2016) -
Block Structure vs. Scope Extrusion: Between Innocence and Omniscience
(IfCoLog (International Federation of Computational Logic), 2016-08-17)We study the semantic meaning of block structure using game semantics and introduce the notion of block-innocent strategies, which turns out to characterise call-by-value computation with block-allocated storage through ... -
Studying Maximum Information Leakage Using Karush-Kuhn-Tucker Conditions
When studying the information leakage in programs or protocols, a natural question arises: "what is the worst case scenario?". This problem of identifying the maximal leakage can be seen as a channel capacity problem in ... -
Algebraic Foundations for Information Theoretical, Probabilistic and Guessability measures of Information Flow
Several mathematical ideas have been investigated for Quantitative Information Flow. Information theory, probability, guessability are the main ideas in most proposals. They aim to quantify how much information is leaked, ... -
Full abstraction for PCF
(2000-12-15) -
Support Vector Motion Clustering
(2017-11) -
Concurrent Bounded Model Checking
(ACM, 2015-02) -
Self-composition by Symbolic Execution
(Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2013)Self-composition is a logical formulation of non-interference, a high-level security property that guarantees the absence of illicit information leakages through executing programs. In order to capture program executions, ...