The probabilistic abstract interpretation framework of neural network analysis analyzes a neural network by analyzing its density distribution flow of all possible inputs. The grids approximation is one of abstract domains the framework uses which abstracts concrete space into grids. In this paper, we introduce two novel approximation methods: distribution approximation and clusters approximation. We show how these two methods work in theory with corresponding abstract transformers with help of illustrations of some simple examples.

Probabilistic abstract interpretation is a theory used to extract particular properties of a computer program when it is infeasible to test every single inputs. In this paper we apply the theory on neural networks for the same purpose: to analyse density distribution flow of all possible inputs of a neural network when a network has uncountably many or countable but infinitely many inputs. We show how this theoretical framework works in neural networks and then discuss different abstract domains and corresponding Moore-Penrose pseudo-inverses together with abstract transformers used in the framework. We also present experimental examples to show how this framework helps to analyse real world problems.

In this paper, we investigate the performances of tunable quantum neural networks in the Quantum Probably Approximately Correct (QPAC) learning framework. Tunable neural networks are quantum circuits made of multi-controlled X gates. By tuning the set of controls these circuits are able to approximate any Boolean functions. This architecture is particularly suited to be used in the QPAC-learning framework as it can handle the superposition produced by the oracle. In order to tune the network so that it can approximate a target concept, we have devised and implemented an algorithm based on amplitude amplification. The numerical results show that this approach can efficiently learn concepts from a simple class.

In this paper, we study the tunable quantum neural network architecture in the quantum exact learning framework with access to a uniform quantum example oracle. We present an approach that uses amplitude amplification to correctly tune the network to the target concept. We applied our approach to the class of positive $k$-juntas and found that $O(n^22^k)$ quantum examples are sufficient with experimental results seemingly showing that a tighter upper bound is possible.

In this paper we propose a new approach to quantum neural networks. Our multi-layer architecture avoids the use of measurements that usually emulate the non-linear activation functions which are characteristic of the classical neural networks. Despite this, our proposed architecture is still able to learn any Boolean function. This ability arises from the correspondence that exists between a Boolean function and a particular quantum circuit made out of multi-controlled NOT gates. This correspondence is built via a polynomial representation of the function called the algebraic normal form. We use this construction to introduce the idea of a generic quantum circuit whose gates can be tuned to learn any Boolean functions. In order to perform the learning task, we have devised an algorithm that leverages the absence of measurements. When presented with a superposition of all the binary inputs of length $n$, the network can learn the target function in at most $n+1$ updates.

Neural approaches to program synthesis and understanding have proliferated widely in the last few years; at the same time graph based neural networks have become a promising new tool. This work aims to be the first empirical study comparing the effectiveness of natural language models and static analysis graph based models in representing programs in deep learning systems. It compares graph convolutional networks using different graph representations in the task of program embedding. It shows that the sparsity of control flow graphs and the implicit aggregation of graph convolutional networks cause these models to perform worse than naive models. Therefore it concludes that simply augmenting purely linguistic or statistical models with formal information does not perform well due to the nuanced nature of formal properties introducing more noise than structure for graph convolutional networks.

In order to support, for example, a quantitative analysis of various algorithms, protocols etc. probabilistic features have been introduced into a number of programming languages and calculi. It is by now quite standard to define the formal semantics of (various) probabilistic languages, for example, in terms of Discrete Time Markov Chains (DTMCs). In most cases however the probabilities involved are represented by constants, i.e. one deals with static probabilities. In this paper we investigate a semantical framework which allows for changing, i.e. dynamic probabilities which is still based on time-homogenous DTMCs, i.e. the transition matrix representing the semantics of a program does not change over time.

In order to perform probabilistic program analysis we need to consider probabilistic languages or languages with a probabilistic semantics, as well as a corresponding framework for the analysis which is able to accommodate probabilistic properties and properties of probabilistic computations. To this purpose we investigate the relationship between three different types of probabilistic semantics for a core imperative language, namely Kozen's Fixpoint Semantics, our Linear Operator Semantics and probabilistic versions of Maximal Trace Semantics. We also discuss the relationship between Probabilistic Abstract Interpretation (PAI) and statistical or linear regression analysis. While classical Abstract Interpretation, based on Galois connection, allows only for worst-case analyses, the use of the Moore-Penrose pseudo inverse in PAI opens the possibility of exploiting statistical and noisy observations in order to analyse and identify various system properties.

Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption, and more generally to optimize a given program. Essentially, it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. Unfolding is one of the basic operations used by most program transformation systems and consists of the replacement of a procedure call by its definition. While there is a large body of literature on the transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages. This paper defines an unfolding system for Constraint Handling Rules programs. We define an unfolding rule, show its correctness and discuss some conditions that can be used to delete an unfolded rule while preserving the program meaning. We also prove that, under some suitable conditions, confluence and termination are preserved by the above transformation.

For deterministic and probabilistic programs we investigate the problem of program synthesis and program optimisation (with respect to non-functional properties) in the general setting of global optimisation. This approach is based on the representation of the semantics of programs and program fragments in terms of linear operators, i.e. as matrices. We exploit in particular the fact that we can automatically generate the representation of the semantics of elementary blocks. These can then can be used in order to compositionally assemble the semantics of a whole program, i.e. the generator of the corresponding Discrete Time Markov Chain (DTMC). We also utilise a generalised version of Abstract Interpretation suitable for this linear algebraic or functional analytical framework in order to formulate semantical constraints (invariants) and optimisation objectives (for example performance requirements).

The automatic generation or synthesis and optimisation of code is an extremely complex task, nevertheless it constitutes to some extend the holy grail of software engineering. In this paper we consider an approach to this problem via a non-standard semantical model of programs in terms of linear operator or, simply, as matrices. This allows us to employ well-developed techniques of classical mathematical (non-linear) optimisation. More concretely we describe here an experimental implementation of the framework which treats programs more than dynamical systems than as logical entities. In this setting we then aim in generating or transforming programs on the basis of optimising some of their properties. In this way we try to end up with code that exhibits the desired properties (at least as much as possible). The initial motivation of this approach can be traced back to when we considered Kocher’s attack on the RSA algorithm [3, 5]. In very simple terms [7]: the problems is that the execution time of a certain algorithm (e.g. modular exponentiation) is based on some secrete or high information (concretely, the bits in a secrete key) and thus it is possible to reveal or extract the secret by analysing the running time. For example we have repeatedly, for each bit k[i] to execute code which takes very little or a lot of time: if k[i] then 〈short〉 else 〈long〉 fi. In, for example, [1] it has been suggested to obfuscate the time signature by using depleted versions [short] and [long] of 〈short〉 and 〈long〉, respectively; i.e. code which is executed in the same time as the original version but which does otherwise not change the state in any way. This padding means that we are replacing if k[i] then 〈short〉 else 〈long〉 fi by if k[i] then 〈short〉; [long] else [short]; 〈long〉 fi. The result is then that both branches always take the same maximal time to execute. As there is a tradeoff between how easy it is to obtain the secrete (key) from the time signature and the increased running time we suggested to introduce the extra time randomly. The result is a whole manifold of programs P(p) in which the padding is performed with a certain probability p or the original code is executed with probability 1− p. The idea is now to find the p∗ for which we have the optimal balance between extra cost and security. The purpose of this paper is to extend this idea to allow the generation or transformation of programs as an optimisation problem. We will consider a whole family of programs parameterised by a large number of variables λi and try to identify those which fulfil certain requirements in an optimal way.

For a simple probabilistic language we present a semantics based on linear operators on infinite dimensional Hilbert spaces. We show the equivalence of this semantics with a standard operational one and we discuss its relationship with the well-known denotational semantics introduced by Kozen. For probabilistic programs, it is typical to use Banach spaces and their norm topology to model the properties to be analysed (observables). We discuss the advantages in considering instead Hilbert spaces as denotational domains, and we present a weak limit construction of the semantics of probabilistic programs which is based on the inner product structure of this space, i.e. the duality between states and observables.

In this chapter, we will describe, in a tutorial style, recent work on the use of fluid approximation techniques in the context of stochastic model checking. We will discuss the theoretical background and the algorithms working out an example. This approach is designed for population models, in which a (large) number of individual agents interact, which give rise to continuous time Markov chain (CTMC) models with a very large state space. We then focus on properties of individual agents in the system, specified by Continuous Stochastic Logic (CSL) formulae, and use fluid approximation techniques (specifically, the so called fast simulation) to check those properties. We will show that verification of such CSL formulae reduces to the computation of reachability probabilities in a special kind of timeinhomogeneous CTMC with a small state space, in which both the rates and the structure of the CTMC can change (discontinuously) with time. In this tutorial, we will discuss only briefly the theoretical issues behind the approach, like the decidability of the method and the consistency of the approximation scheme.

Speculative optimisation relies on the estimation of the probabilities that certain properties of the control flow are fulfilled. Concrete or estimated branch probabilities can be used for searching and constructing advantageous speculative and bookkeeping transformations. We present a probabilistic extension of the classical equational approach to data-flow analysis that can be used to this purpose. More precisely, we show how the probabilistic information introduced in a control flow graph by branch prediction can be used to extract a system of linear equations from a program and present a method for calculating correct (numerical) solutions.

Citation for published version: Broadbent, A, Fitzsimons, J & Kashefi, E 2010, Measurement-Based and Universal Blind Quantum Computation. in A Aldini, M Bernardo, A Di Pierro & H Wiklicky (eds), Formal Methods for Quantitative Aspects of Programming Languages: 10th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2010, Bertinoro, Italy, June 21-26, 2010, Advanced Lectures. Lecture Notes in Computer Science, vol. 6154, Springer Berlin Heidelberg, pp. 43-86. https://doi.org/10.1007/978-3-642-13678-8_2

We develop a new notion of security against timing attacks where the attacker is able to simultaneously observe the execution time of a program and the probability of the values of low variables. We then propose an algorithm which computes an estimate of the security of a program with respect to this notion in terms of timing leakage and show how to use this estimate for cost optimisation.

Semantics-based program analysis uses an abstract semantics of programs/systems to statically determine run-time properties. Classic examples from compiler technology include analyses to support constant propagation and constant folding transformations and estimation of pointer values to prevent buffer overruns. More recent examples include the estimation of information flows (to enforce security constraints) and estimation of non-functional properties such as timing (to determine worst case execution times in hard real-time applications). The classical approaches are based on semantics involving discrete mathematics. Paralleling trends in model-checking, there have been recent moves towards using probabilistic and quantitative methods in program analysis. In this paper we start by reviewing both classical and probabilistic/quantitative approaches to program analysis. We shall provide a comparison of the two approaches. We shall use a simple information flow analysis to exemplify the classical approach. The existence of covert information flows through timing channels are difficult to detect using classical techniques; we show how such problems can be addressed using probabilistic techniques.