 Previous Grad Seminars
|
Tidigare doktorandseminarier i teoretisk datalogi /
Previous PhD Student Seminars in Theoretical Computer Science
Se även
tidigare terminers seminarier.
See also
PhD student seminars previous terms.
Informal Seminars Spring 2010
-
26 May 2011 15:15 room 1537
Unique Games on Hypercubes
(Michael Belfrage)
The Unique Games Conjecture is one of the most intriguing open
problems in theoretical computer science. Should it turn out to
be true, then this would have striking implications for a long list
of well studied optimization problems; namely, tight inapproximability
bounds.
In this talk, I will give a brief introduction to the conjecture,
its implications, and the larger context. The main focus is then
on algorithmic approaches to shed more light on the truth of the
conjecture. In particular, I will present efficient and near-optimal
algorithms for hypercubes in the average case. The introduced propagation
using plurality technique might be of independent interest.
-
25 May 2011 14:15 room 1537
Rehearsal Talk: Santa Claus Schedules Jobs on Unrelated Machines
(Ola Svensson, KTH CSC)
One of the classic results in scheduling theory is the 2-approximation
algorithm by Lenstra, Shmoys, and Tardos for the problem of scheduling
jobs to minimize makespan on unrelated machines, i.e., job j requires
time p_{ij} if processed on machine i. More than two decades after its
introduction it is still the algorithm of choice even in the restricted
model where processing times are of the form p_ij \in {p_j, \infty\}.
This problem, also known as the restricted assignment problem, is
NP-hard to approximate within a factor less than 1.5 which is also the
best known lower bound for the general version.
Our main result is a polynomial time algorithm that estimates the
optimal makespan of the restricted assignment problem within a factor
33/17 + \epsilon \approx 1.9412 + \epsilon, where $\epsilon > 0$ is an
arbitrarily small constant. The result is obtained by upper bounding the
integrality gap of a certain strong linear program, known as
configuration LP, that was previously successfully used for the related
Santa Claus problem. Similar to the strongest analysis for that problem
our proof is based on a local search algorithm that will eventually find
a schedule of the mentioned approximation guarantee, but is not known to
converge in polynomial time.
-
24 May 2011 13:15 room 1537
Rehearsal talk for PLAS'11
(Musard Balliu, KTH CSC)
Temporal epistemic logic is a well-established framework for expressing agents knowledge and how it evolves over time. Within language-based security these are central issues, for instance in the context of declassification. We propose to bring these two areas together. The paper presents a computational model and an epistemic temporal logic used to reason about knowledge acquired by observing program outputs. This approach is shown to elegantly capture standard notions of noninterference and declassification in the literature as well as information flow properties where sensitive and public data intermingle in delicate ways.
-
23 May 2011 13:15 room 1537
Open Problems in TCS: Resolution, Gröbner bases and space complexity
(Jakob Nordström, KTH CSC)
The best SAT solvers known today are based on the so-called DPLL method,
which uses the proof system resolution. Another possibility is to
translate CNF formulas to polynomial equations and run the Gröbner basis
algorithm. This corresponds to a proof system known as Polynomial
Calculus. However, while Polynomial Calculus is known to be stronger than
resolution, it is still the case that SAT solvers based on the latter
system clearly outperform those based on the former.
An interesting problem is to understand the theoretical potential and
limitations of Polynomial Calculus. For instance, given an unsatisfiable
3-CNF formula, how space-efficiently in general can Polynomial Calculus
prove that the formula is contradictory? While the answer to the
corresponding question for resolution was solved over a decade ago, the
case of Polynomial Calculus remains open.
In this talk, I will give a survey of what has been shown and try to
indicate why known approaches do not seem to work. The talk will be mostly
based on the paper "Space Complexity in Propositional Calculus" by
Alekhnovich, Ben-Sasson, Razborov, and Wigderson published in SIAM Journal
on Computing 2002, although my exposition will probably be somewhat
different.
-
24 Mar 2011 10:15 room 4523
A Zero-One Law for Secure Multi-Party Computation with Ternary Outputs
(Gunnar Kreitz, KTH CSC)
-
07 Mar 2011 13:15 room 1537
Locking the Throne Room - ECMA Script 5, a frozen DOM and the eradication of XSS
(Mario Heiderich, Ruhr University, Germany)
Cross Site Scripting has been a topic in countless presentations over the last decade. That easy to grasp but hard to solve problem has been shaking the web and caused major trouble on hundreds to thousands of high traffic and commercial and well as governmental websites. Mitigation techniques have been developed and discussed in depth - starting with restrictive content filters, educational programs and trainings, programmer's best practices and guidelines, proxy filters and many more. Still XSS remains a major problem far from being solved. The multilayer model on which the web relies causes too much reciprocity to find an easy cure - and the DOM as the actually affected layer is still lying unprotected open for the attacker.
This presentation introduces and discusses a novel approach of encountering XSS and similar attack techniques by making use of several new features included in the ECMA Script 5 specification draft. It will be shown how to create a simple JavaScript to seal important DOM properties, and take away the attackers ability to read and modify sensitive data in a tamper resistant and light-weighted way - without being "too loud". Modern browsers, such as Chrome 8 and Firefox 4, for the first time provide the possibility of creating and using client side IDS/IPS systems, written in JavaScript and running without special execution privileges. The presentation will show how these work, what the implications are, and what the future of XSS mitigation and eradication might look like.
-
01 Mar 2011 15:15 room 4523
A survey of superoptimisers
(Jesper Särnesjö)
Jesper Särnesjö will present the literature study
for his masters thesis on superoptimisers.
Superoptimisers search for optimal assembly sequences given a goal
function. He will speak about four implementatons: Henry Massalin's
original work from 1987; the GNU superoptimiser written by Torbjörn
Granlund; Denali, a project started at Compaq Systems Research, and the
superoptimisers that is the focus of Sorav Bansal's thesis at
Stanford. He will discuss how they differ in usage areas and in handling
of input and output, how they measure optimality, which search
strategies they use, and how they determine if two programs are
equivalent.
-
17 Jan 2011 13:15 room 1537
Hasse Diagram Generators and Petri Nets
(Mateus Oliveira)
In [LJ06] Lorenz and Juhas raised the question of whether there exists
a suitable formalism for the representation of infinite families of
partial orders generated by Petri nets. Restricting ourselves to
bounded p/t-nets, we propose "Hasse diagram generators" as an answer.
We show that Hasse diagram generators are expressive enough to
represent the partial order language of any bounded p/t-net. We prove
as well that it is decidable both whether the (possible infinite)
family of partial orders represented by a given Hasse diagram
generator is included on the partial order language of a given p/t-net
and whether their intersection is empty. Based on this decidability
result, we prove that the partial order languages of two given Petri
nets can be effectively compared with respect to inclusion. Finally we
address the synthesis of k-safe p/t-nets from Hasse diagram
generators.
-
Oct 15 2010 13:15 room 1537
Rehearsal talk on Inferring Compact Models of Communication Protocol Entities
(Siavash Soleimanifard, KTH CSC)
Model-based techniques for verification, testing,
and validation of commmunication protocols, including
model checking and model-based testing,
have witnessed drastic advances in the last decades.
They require access to a formal model that
specifies the behavior of protocol entities, which
ideally should be developed during specification and design.
It is therefore important to develop automated techniques that support
the task of producing models, e.g., models that reflect the behavior
of an existing protocol implementation. A potential approach is to use
program analysis to construct models from source code. However, many system
components, such as library modules, or third-party components, often
do not allow analysis of source code.
We will therefore focus on techniques for constructing models from
observations of their external behavior.
Our overall goal is to support model-based approaches to
verification and validation of communication protocols by
techniques that automatically generate models of
communication protocol entities from observations of their
external behavior, using techniques based on regular
inference (aka automata learning). In this talk, I will address
the problem that existing regular inference techniques produce ``flat'' state
machines, whereas practically useful protocol models structure
the internal state in terms of control locations and state variables,
and describes dynamic behavior in a suitable (abstract) programming notation.
We present a technique for introducing structure of an unstructured
finite-state machine by introducing state variables and program-like
descriptions of dynamic behavior, given a certain amount of user
guidance. Our technique groups states with ``similar control behavior'' into control locations,
and obtain program-like descriptions by means of decision tree generation.
We have applied parts of our approach to an executable state machine
specification of the Mobile Arts Advanced Mobile Location Center
(A-MLC) protocol and evaluated the results by comparing them to the
original specification.
-
June 4 2010 13:15 1537
Procedure-Modular Verification of Control Flow Safety Properties
(Siavash Soleimanifard, KTH CSC)
Modularity is a design paradigm that aims at controlling
the complexity of developing large software and facilitates
the reuse of components. When applied to verification, i.e.,
to establish the formal correctness of a software product,
modularity requires that correctness of the software modules
(components) is specified and verified independently
(locally) for each module, while the correctness of the whole
system is specified through a global property, the correctness
of which is verified relative to the local specifications rather
than relative to the actual implementations of the modules.
Such an approach allows an independent evolution of the
implementations of individual modules, only requiring the
re--establishment of their local correctness (provided the local
specifications have not changed).
In this talk, I will describe a novel technique for fully automated
procedure--modular verification of Java programs equipped
with method--local and global assertions that specify safety
properties of sequences of method invocations. Modularity
of verification is achieved by relativizing the correctness of
global properties on the local properties rather than on the
implementations of methods, and is based on the construction
of maximal models. I will also introduce ProMoVer,
which is our tool support for the technique. At the end of my talk
I will demonstrate usage of ProMoVer in a short demo.
-
March 1 2010 13:15 1537
Spotify's music streaming protocol
(Gunnar Kreitz, KTH CSC)
Spotify is a music streaming service offering a large library of
licensed music for immediate playback. Streaming is done from a
server-assisted peer-to-peer network, where our servers help guarantee
availability and keep latency down, while the p2p network helps by
offloading our servers.
I will give an overview of, and describe some details of, the Spotify
music streaming protocol. This seminar will likely be a bit more
practical than most seminars in this series.
-
Tuesday February 16, 10:30-12:00, room 4523:
Approximating Max-Min and Min-Max Allocation Problems
(Ola Svensson, KTH CSC)
I will survey some of the recent results regarding the problem
"Max-Min fair allocation" of allocating n resources to m players
so as to maximize the happiness of the least happy player.
We will analyze a strong linear programming formulation
(known as Configuration LP) for this problem and show that it has
integrality gap of at most 1/5.
As the considered problem and the classic scheduling problem of
minimizing the maximum load have a similar structure
--- only the objective functions differ ---
this gives hope that we can use a similar approach for the
scheduling problem. I have some encouraging preliminary results
in this direction but the main problems (that we hopefully can
resolve together) are still open.
References:
The results I planned to cover are in the following articles:
http://portal.acm.org/citation.cfm?id=1132522
http://www.wisdom.weizmann.ac.il/~feige/mypapers/santaclaus1.pdf
-
Monday June 15, 13.15, room 1537 (Lindstedtsvägen 5, floor 5):
Some highlights from STOC 2009
(Per Austrin, KTH)
STOC 2009 recently took place in Washington and it contained some very
nice results, of which I will describe a few.
In an attempt to make it interesting for everyone, I will primarily
focus on broad results of interest to theoreticians in general and not
so much on the specialized results in various subfields. In addition
I will mostly state problems (with motivations) and results, and not
give many proofs (if any).
It will be an informal presentation and I will continue until either
me or the audience becomes too tired.
Avklarade doktorandseminarier höstterminen 2008
/ Seminars Held Fall 2008
-
Friday December 19, 10:15, room 1439:
Att vinna mer än andra -- Om flerpersoners spel utan överförbar utilitet
(Erik Gustafsson)
-
Matematiska spel finns i många varianter, alla med sina egna svårigheter.
Har spelen fler än två spelare, är det viktigt för spelarna att uppnå en viss grad av samarbete,
men det finns inga självklara regler för hur detta ska gå till.
Om avtal sluts, saknas kontrollmekanismer för att genomföra dessa avtal, och tänkbara lösningar blir instabila.
Problemet försvåras ytterliggare av att belöningen för ett lyckat samarbete inte går att fördela fritt mellan spelarna.
Det finns ett flertal förslag till metoder för att lösa dessa spel, men ingen är riktigt tillfredsställande.
Att hitta en objektiv lösning för denna typ av spel är ett öppet problem inom spelteorin.
-
Friday November 14, 10:00, room 1439:
Secure and confidential applications on UICC
(Lasse Edlund)
-
Mobile operators today are looking for new technologies to add to their
existing services. Services that add value and generate income could be
different kinds of proximity payment and entrance systems using NFC
technology. This kind of short range radio technology is new and there
have been no real implementations of banking or entrance system for
mobile phones aside from a few trials. The main goal is to let the
mobile phones replace the need for various RFID and magnetic cards used
today.
This thesis investigates how to manage multiple applications on a
single UICC, this way many different actors can share a single hardware
resource.
Usually a smart card given for these services is owned by the service
provider, but in our case the SIM card is owned and managed by the
Mobile Network Operators. In order to be able to delegate rights and
maintain security in an unsafe environment there has been different
standards and ideas proposed to solve all issues.
Some of these proposals run along the interests of mobile operators,
others of financial institutions but they all want to achieve the same
goal increasing revenue.
This is only possible if all parts of this economic ecosystem gets a
part of the financial gain in a fair way.
There are trials ongoing with mobile NFC technology that replaces
credit cards and many actors companies have shown interest in using
the mobile phone’s secure and contactless interface to replace existing
security devices.
-
Monday March 10, 13:00, room 1537:
A language extension for provably safe exception handling
(Bart Jacobs,
Department of Computer Science,
Katholieke Universiteit Leuven,
Belgium)
-
Most modern programming languages include an exception throwing
construct for safely and easily dealing with unlikely
conditions. However, they typically also include constructs for
catching exceptions. This creates a safety risk. Furthermore, in a
multithreaded program, even in the absence of catch constructs, an
exception typically terminates the thread but not the entire
program. As a result, writing provably safe programs is difficult. We
propose a new language construct, called subsystems, to facilitate
writing provably safe programs, and proof rules for this construct
that enable proving safety properties in the presence of synchronous
and asynchronous exceptions.
-
Måndag 21 april, kl 13.15, rum 1537:
Broadcast-kryptering – begränsningar och möjligheter
(Gunnar Kreitz,
Teorigruppen,
KTH CSC)
-
Broadcast-kryptering används då en sändare vill skicka krypterad data
till en grupp mottagare som ändras med tiden. Typtillämpning är olika
former av mediadistribution som betal-TV och moderna videoformat (t.ex.
Bluray).
Man kan bygga protokoll för broadcast-kryptering baserade på olika
kryptografiska primitiver, där det vanligaste är en pseudo-slump
generator. Jag tänkte prata om en naturlig konstruktion och hur bra
protokoll baserade på den kan bli.
Om tiden och orken räcker till så pratar jag även lite om andra
konstruktioner. Seminariet blir relativt informellt och hålls på
svenska.
-
Måndag 26 maj, kl 14.15, rum 1535
(OBS! tiden och platsen!):
Provably Correct Runtime Monitoring
(Irem Aktug,
Teorigruppen,
KTH CSC)
[slides (updated)
 ]
-
Runtime monitoring is an established technique for enforcing a wide
range of program safety and security properties. A monitor operates by
observing the behavior of a target program and terminating the program
when an action that violates the property is about to occur. Numerous
security applications like firewalls, kernels, memory sandboxes, and
Java stack inspection are based on this principle. Monitors have been
implemented either as external entities that run in parallel with the
target program or through rewriting the program to make it
self-monitoring; these we call
external monitoring and
monitor inlining,
respectively.
In this talk, we present a formalization of monitoring and monitor
inlining for java bytecode programs.
Monitors can be formalized as security automata induced from a
special-purpose monitor specification language, ConSpec.
The automata operate on finite or infinite strings of calls to a fixed
API, allowing local dependencies on parameter values and heap content.
We use a two-level class file annotation scheme to characterize two
key properties of an inlined program:
-
that the program is correct
with
respect to the monitor as a constraint on allowed program behavior,
and
-
that the program has an instance of the given monitor embedded
into
it, which yields state changes at
prescribed points according to the monitor's transition function.
As our main application of these results we describe a concrete
inliner, and use the annotation scheme to characterize its
correctness. For this inliner, correctness of the level II annotations
can be decided efficiently by a weakest precondition annotation
checker, thus allowing on-device checking of inlining correctness in a
proof-carrying code setting.
-
Thursday September 13, 10:00 AM, room 1635
(NB! Not the usual time and place):
On Length, Width and Space in Resolution
(Jakob Nordström,
Theory Group, KTH CSC)
[slides (updated)
]
-
Determining whether a propositional logic formula is a tautology,
i.e., whether it is satified by all truth value assignments,
is a fundamental problem both from
a theoretical and a practical point of view. On the one hand,
it is closely related to central questions
in computational complexity and mathematics
(e.g. the P ≠ NP
millennium problem of the Clay Mathematics Institute).
On the other hand, designing efficient algorithms for proving
tautologies, or equivalently refuting unsatisfiable formulas, is a
very important problem in applied research and in industry, e.g. in
the context of formal methods.
In this talk, we will focus on resolution, which proves
tautologies by showing that their negations, expressed as CNF
formulas, are unsatisfiable. It is arguably the single most studied
propositional proof system, and many real-world automated theorem
provers are based on it.
For resolution, two important complexity measures are the minimum
length of a proof for a formula and the minimum
space of a proof. The length, or number of lines, gives a
lower bound on the time needed for any algorithm producing a
resolution proof, and the space measure tells us the minimum amount of
memory needed while searching for a proof. A third interesting measure
turns out to be the width, which is the maximal
number of variables in any line in the proof.
Studying the measures of length, width and space, and relating
them to one another, can help us devise good heuristics and/or
understand the limitations of different approaches for proving
tautologies.
In the first half of the talk, we will review some of the significant
(and surprising!) results relating length, space and width, and also
try to briefly sketch our own contribution to the area.
In the second half, we will present some interesting open problems,
which should be readily accessible to a general computer science and
mathematics audience.
This talk is a tutorial that will be given at
The
Fall School of Logic and Complexity '07
in the Czech Republic,
and it will therefore be held in English. It is
intended to last for 2x45 minutes.
No prerequisites are needed, apart from a basic knowledge of
(propositional) logic.
Feedback will be most welcome.
-
Monday November 12, 13:15, room 1537:
On the Approximation Resistance of a Random Predicate
(Johan Håstad,
Theory Group, KTH CSC)
[slides
]
-
A predicate is approximation resistant if
no probabilistic polynomial time approximation algorithm can do
significantly better then the naive
algorithm that picks an assignment uniformly
at random. In this talk we discuss predicates
of Boolean inputs where the width of
the predicate is allowed to grow.
Samorodnitsky and Trevisan proved that,
assuming the Unique Games
Conjecture, there is a family of very sparse predicates
that are approximation resistant. We prove that,
again assuming the Unique Games Conjecture,
any predicate implied by their predicate remains approximation
resistant and prove that this condition, with high
probability, applies to a randomly chosen predicate.
-
Monday November 19, 13:15-15:00, room 1537:
On Recent Attacks on Hash Functions
(Martin Ekerå och Henrik Ygge)
[slides
]
-
Cryptographic hash functions play an important role in information
security.
The hash function MD4, introduced by Rivest in 1990, has served as a
template for many other hash functions, such as MD5, SHA-0, SHA-1,
RIPE-MD, RIPE-MD 160 and HAVAL-128 amongst others.
In 2004, Xiaoyun Wang, Dengguo Feng, Xuejia Lai and Hongbo Yu
announced collisions on MD4, MD5, HAVAL-128 and RIPE-MD. These were
the first full collisions to be announced on MD5, HAVAL-128 and RIPE-MD.
The fundamental idea behind Wang's attack is to keep track of how
bitwise differences propagate through the internal states of the hash
function. Therefore, the attack may be mounted against most iterated
hash functions, including more recent functions such as SHA-0 and SHA-1.
No full collision has yet been found on SHA-1, but a theoretical
attack with complexity significantly lower than that of a brute force
collision attack has been presented.
In the first half of the seminar, we will give a general overview of
cryptographic hash functions and Wang's attack. It will require no
prerequisites.
In the second part, we will go into details about how differential
paths are constructed and how they may be used to find collisions in
MD5. This part will get very technical.
The seminar is planned to be held in Swedish, but we can switch to
English if the audience so desires. All slides will be in English. The
intended duration is 2x45 minutes.
-
Måndag 22 januari, kl 13.15-15.00 (ca), rum 1537:
Verifying proofs by reading only 3 bits
(part 3 of 2)
(Johan Håstad,
Theory Group, KTH CSC)
-
In this seminar, Johan will go into some of the intricate details of
the proofs of the theorems discussed in the
seminars
on December 4th and 18th, 2006.
-
Måndag 5 februari, kl 13.15, rum 1537:
The power of Unique Games—verifying a proof by reading
two bits (1/2)
(Per Austrin,
Theory Group, KTH CSC)
[slides
]
-
In these two talks (second talk on Feb 12),
we give an introduction to the so called Unique
Games Conjecture, which during the last years has established itself
as one of the most important open questions in computational
complexity.
In the first part we state the conjecture and give a general survey of
the many nice implications of the conjecture (and its variations).
Time and interest permitting, we will also survey possible attempts at
proving or disproving the conjecture, and how far they have lead.
The talk aims to be generally accessible and no prior encounters with
the subject are required.
-
Måndag 12 februari, kl 13.15, rum 1537:
The power of Unique Games—verifying a proof by reading
two bits (2/2)
(Per Austrin,
Theory Group, KTH CSC)
-
In these two talks (first talk on Feb 5),
we give an introduction to the so called Unique
Games Conjecture, which during the last years has established itself
as one of the most important open questions in computational
complexity.
The second part will be more technical than the previous one, as we
dig into some of the details of using the UGC to obtain tight
inapproximability for the Max-Cut problem, including some deep results
from Fourier analysis.
Though a bit technical, the talk aims to be more or less
self-contained.
-
Måndag 21 maj, kl 13.15, rum 1537:
Induction Revisited - Proofs in the First-Order Mu-Calculus
(Mads Dam,
Theory Group, KTH CSC)
-
Induction is the fundamental mechanism available to allow finite
arguments to
support conclusions on infinite objects. The approaches taken to induction
in the literature differ widely in how suitable they are for mechanisation.
The first-order, or relational, mu-calculus is the least extension of
first-order logic closed under inductive, formally monotone definitions, and
so offers a natural setting in which to study proof principles for
induction. In the talk we survey some approaches to induction
in the literature, and then concentrate on global induction, an
approach, introduced originally by Dam and Gurov, which uses a global
rule of discharge to ensure that inductive arguments are well-founded.
Global induction has been implemented in a theorem prover, EVT, which
has been
used to formalize programming languages and calculi such as CCS, the
pi-calculus, a simple threaded Java virtual machine, and, as the by far
largest experiment, the concurrent functional language Erlang.
We examine various semantic and syntactic versions of the discharge
condition, and give, in particular, an automata-theoretic characterization,
based on Streett automata, which is suitable for practical proofs.
Further, given time, we show that the proof-theoretic power of global
induction
as considered here coincides with that of well-founded induction.
The results have been obtained in joint work with Christoph Sprenger.
|
