Provable security for low level execution platforms
Much attention has been paid in the recent years to the
problem of verification for various types of low level execution
platforms such as OS kernels, device drivers, hypervisors, and
cryptographic software. In the course we cover a range of topics
related to this problem: Formulating correct and relevant verification
goals, formally modelling the hardware platforms and security
requirements, and formally verifying that the requirements are met.
We start in a rather idealised setting suitable for very simple hardware
platforms such as those found in legacy embedded control systems,
and gradually add system features such as virtual memory, devices
and IO, and caches, and examine how the formalisations and
verification approaches are adapted. The course presupposes
familiarity with first order logic, the use of first order logic
for modelling of computer systems, transition system semantics,
and, preferably also some basic familiarity with processor architecture.
At the end of the course the student should be able to independently
model a piece of simple sequential system software and verify
it at the level of transition system semantics against a high level
Distributed models, MapReduce and large scale algorithms
As a fundamental tool in modeling and analyzing real world data, large-scale algorithms are a central part of any tool set for big data analysis. Processing datasets with hundreds of billions of entries is only possible via developing distributed algorithms under distributed frameworks such as MapReduce, Pregel, Gigraph, and alike. For these distributed algorithms to work well in practice, we need to take into account several metrics such as the number of rounds of computation and the communication complexity of each round. For example, given the popularity and ease-of-use of MapReduce framework, developing practical algorithms with good theoretical guarantees for basic algorithmic primitives is a problem of great importance.
In this course, we discuss how to design and implement algorithms based on traditional MapReduce architecture. In this regard, we discuss various basic algorithmic problems such as computing connected components, maximum matching, MST, counting triangle, clustering, diversity maximization and so on so for. In particular, we discuss a computation model for MapReduce and describe the sampling&filtering, local random walk, and core-set techniques to develop efficient algorithms in this framework.
Elements of Quantum Computation
This course aims to introduce the basic notions of quantum computing with
particular emphasis on quantum algorithms. We will discuss basic quantum
physical concepts - like Observable, State and Measurement - as well as
central aspects of Quantum Computing - including Quantum Bits (qubits) and
registers, Quantum Evolution, Quantum Circuits, Quantum Teleportation and the
basic Quantum Algorithms known at the present time.
The lectures will cover: Introduction to Quantum Mechanics, Quantum Bits and
Complex Vector Spaces, Quantum Evolution and Quantum Gates, Quantum Registers,
No-Cloning Theorem, Quantum Key Distribution/Cryptography, Quantum
Entanglement and Teleportation, Quantum Algorithms and Circuits, Quantum
Search (Grover's Algorithm), Quantum Fourier Transform, Quantum Factoring of
Integers (Shor's Algorithm); and possibly: further Quantum Algorithms,
alternative Quantum Computing Models, Quantum Error Correction.
As pre-requisites we will assume a basic knowledge of basic Linear Algebra
(i.e. vectors, matrices, basis, inner product, etc.)
- Noson S. Yanofsky, Mirco A. Mannucci:
Quantum Computing for Computer Scientists,
Cambridge University Press, 2008
- Eleanor Rieffel, Wolfgang Polak:
Quantum Computing, A Gentle Introduction.
MIT Press, 2014
- Richard J. Lipton, Kenneth W. Regan:
Quantum Algorithms via Linear Algebra.
MIT Press, 2014
- Phillip Kaye, Raymond Laflamme, Michael Mosca:
An Introduction to Quantum Computing,
Oxford University Press 2007
An Introduction to Quantum Computing
- E.Rieffel, W.Polak:
An introduction to quantum computing for non-physicists.
ACM Computing Surveys, 2000