Warning: You are viewing outdated content. The current TCS webpage is here.

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 2016

01 Apr 2016 at 10:15 in 4room 4523, Lindstedtsvägen 5
On Dinur's Proof of the PCP Theorem
(Adam Schill Collberg, Susanna F. de Rezende, Jan Elffers, and Johan Westerborn, KTH)

Probabilistically checkable proofs are proofs that can be checked by randomized algorithms reading very few bits of the proof. In the early 1990s, it was shown that proofs for NP statements could be transformed into probabilistically checkable proofs with only a modest increase in their size. This so-called PCP theorem is considered one of the crowning achievements of theoretical computer science. The proof of this theorem was technically intricate and highly nontrivial, however. In 2005, Irit Dinur gave a dramatically simpler (and radically new) construction of probabilistically checkable proofs. In this talk, we will present Dinur's construction, closely following a survey paper by Jaikumar Radhakrishnan and Madhu Sudan (http://www.ams.org/journals/bull/2007-44-01/S0273-0979-06-01143-8/). We will start by explaining the notion of a probabilistically checkable proof, then present the formal definitions, and finally go through Dinur's proof in detail.
14 Jan 2016 at 13:15 in room 1625
Zero-Knowledge proofs for all NP-languages
(Martin Bullinger, KTH)

Proving membership in a language without conveying any other information is a powerful tool and performed by zero-knowledge proofs.
Based on computational zero-knowledge, I will first sketch, how to extend the interactive proof system from class for GraphNonIsomorphism into a zero-knowledge proof.
Under the assumption that secure encryption functions exist, I will argue why zero-knowledge proofs for all languages in NP exist. With similar ideas as above, a zero-knowledge protocol for 3-Coloring will be obtained and with the NP-completeness of this language, the assertion will follow.

Informal Seminars Fall 2015

07 Jul 2015 at 14:00 in room 4523
Locally Dense Codes
(Jan Elffers, KTH)

I will present the paper "Locally Dense Codes" by Micciancio (CCC 2014).
This paper is about nearest codeword problems for linear binary codes with respect to the hamming distance (L1) norm. The two problems considered are the the Nearest Codeword Problem (NCP) and the Minimum Distance Problem (MDP). MDP is a special case of NCP; both MDP and NCP are NP-hard. NP-hardness proofs of MDP polynomially reduce NCP to MDP. In this reduction, a gadget called a locally dense code is used. This is a linear code with large minimum distance d that admits a ball of smaller radius r<d containing an exponential number of codewords, together with some auxiliary information used to map these codewords.
07 Jul 2015 at 13:00 in room 4523
Small explicit expander graphs
(Marc Vinyals, KTH)

Large expander graphs are easy to come with since random graphs are good expanders almost surely, and it is even possible to construct them deterministically. Extremely small expanders can just be enumerated.
We will see a deceptively simple construction that is useful for graph sizes in between, and show how algebra and number theory play a role in analysing its properties.
This talk is based on the paper "Ramanujan Graphs" by Lubotzky, Phillips and Sarnak.
25 Jun 2015 at 15:00 in room 4523
Undirected Connectivity is in Log-Space
(Mladen Miksa, KTH)

If we need to compute some function, how much time or memory will we need to produce the result? What if we are given access to some random bits? Can we do better then? This question is one of the big open problems in computational complexity and comes in many different flavors. In one instance of this question, we ask whether randomness helps a machine that is allowed to use at most logarithmic space. That is, we ask whether L = RL? As a stepping stone towards proving this equality, we can try to devise deterministic log-space algorithms for problems that we know are in RL. An example of such a problem is undirected connectivity, in which we are given an undirected graph and two vertices s and t, and we want to know if there is a path between s and t. A randomized log-space algorithm for this problem was formulated by Aleliunas, Karp, Lipton, Lovasz, and Rackoff in '79, and the question whether there is a deterministic algorithm remained an open problem for a number of years. In this talk, I will present the result by Reingold that there is indeed a deterministic log-space algorithm for solving undirected connectivity, which moves us one step closer to understanding randomness and proving that L = RL.
25 Jun 2015 at 14:00 in room 4523
Algebraic Algorithms for Matching and Matroid Problems
(Susanna F. de Rezende, KTH)

We will present the paper "Algebraic Algorithms for Matching and Matroid Problems" by Nicholas J. A. Harvey (http://dx.doi.org/10.1137/070684008). This paper uses algebraic techniques to obtain algorithms for two well-known combinatorial problems: non-bipartite matching and matroid intersection.
In 1979, Lovász first used polynomial identity testing to test for matchings. Rabin and Vazirani, in 1987, showed how to compute perfect matchings in general graphs in time $O(n^{\omega+1})$. More recently, Mucha and Sankowski show how to find a perfect matching in general graphs in time $O(n^\omega)$. This paper yields a new randomized algorithm that matches the efficiency of Mucha and Sankowski's and has the advantage that it is a purely algebraic algorithm.
We will first present a simple algorithm that uses polynomial identity testing to find a perfect matching in bipartite graphs and then present Harvey's algorithm for general graphs. If time permits, we will briefly talk about the other algorithm in this paper, for matroid intersection, that also relies on algebraic properties.
25 Jun 2015 at 13:00 in room 4523
A Note on Ramsey Numbers
(Adam Schill Collberg, KTH-TCS)

In this talk I will present the paper "A Note on Ramsey Numbers" from 1980 by Ajtai, Komlós and Szemerédi. Recall that the Ramsey number R(s,t) denotes the smallest positive integer such that a graph on R(s,t) vertices must contain either an s-clique or an independent set of size t. While it is very difficult to exactly determine R(s,t) for non-trivial s and t, the asymptotics of this number are of interest and are quite well studied. In this paper the best known (to my knowledge) upper bound for fixed s (or symmetrically t) when s != t is obtained, namely it is shown that R(s,t) < c(s) t^{s-1}/(ln(t))^{s-2} for s > 2. In short, this is done by first showing the result for triangle-free graphs with a subgraph removal scheme. Then it is extended to a more general setting by means of the probabilistic method and a clever induction argument. In the interest of time I will try to refrain from going into technicalities and focus on conveying the ideas of the results and their proofs. Should there be time left however, we might go into more detail.
11 Jun 2015 at 10:15 in room 1535
A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds
(Mladen Miksa, KTH)

We study the problem of obtaining lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et al. '99] also on proof size. [Alekhnovich and Razborov '03] established that if the clause-variable incidence graph of a CNF formula F is a good enough expander, then proving that F is unsatisfiable requires high PC/PCR degree. We further develop the techniques in [AR03] to show that if one can "cluster" clauses and variables in a way that "respects the structure" of the formula in a certain sense, then it is sufficient that the incidence graph of this clustered version is an expander. As a corollary of this, we prove that the functional pigeonhole principle (FPHP) formulas require high PC/PCR degree when restricted to constant-degree expander graphs. This answers an open question in [Razborov '02], and also implies that the standard CNF encoding of the FPHP formulas requires exponential proof size in polynomial calculus resolution. Thus, while Onto-FPHP formulas are easy for polynomial calculus, as shown in [Riis '93], both FPHP and Onto-PHP formulas are hard even when restricted to bounded-degree expanders.

Informal Seminars Spring 2015

13 May 2015 at 15:00 in room 4423
The Rödl Nibble à la Johansson and Bansal et al.
(Adam Schill Collberg, KTH)

I've read a (tentative I think) version of the paper "On the Lovasz Theta function for Independent Sets" by Bansal, Gupta and Guruganesh dealing with approximation of independent set for bounded degree graphs, which Nikhil Bansal very eloquently presented to us a couple of weeks ago. A key component of their algorithmic result is the use of a "nibble" algorithm by Johansson for certain cases of the Sherali-Adams relaxation value. In this seminar we will prove Johansson's (strong) result, which is the following:
For any r, D, there exists a randomized algorithm that, given a graph G with maximum degree D such that the neighborhood of each vertex is r-colorable, outputs a proper coloring of V(G) using O((D*ln(r)/ln(D)) colors in expected poly(n2^D) time.
The proof (which is a, by the authors, modified version of Johansson's) is rather long and probably two hours will not be enough to go through all of it rigorously, but it's somewhat repetitive so it might be enough to give the intuition and ideas for some parts. Further, it uses some classic and/or relatively deep results in probability theory which we'll merely state.

Informal Seminars Fall 2014

13 Nov 2014 at 15:30 in 4523
On conflict driven clause learning — a comparison between theory and practice
(Gustav Sennton, KTH)

The boolean satisifiability (SAT) problem is the canonical NP-complete problem and every other NP-complete problem can be reduced to the SAT problem. Since the SAT problem is NP-complete large instances of this problem should be difficult to solve. However, in practice conflict driven clause learning (CDCL) solvers solve large real-world instances of the SAT problem efficiently. Recently, a theoretical upper bound was shown for the efficiency of a certain version of such solvers, but that solver version differs in several ways from solvers used in practice. In this project experiments are used to investigate whether such a solver is realistic and whether its theoretical bound holds for solvers used in practice. These experiments compare all the components that differ between the theoretical solver version and a real implementation of a solver. The experimental results show that the running times of the two solvers often differ substantially. At the same time, the theoretical running time bound seems to hold for the practical solvers. I.e. the running time of practical solvers seems to grow polynomially for formulas for which the theoretically predicted running time is polynomial. However, some of the formulas used should be tested further since not enough data points have been collected for these formulas. For these formulas we cannot rule out high asymptotical running times of real-world solvers.
22 Oct 2014 at 10:00 in room 1537
Automating Information Flow Analysis of Low Level Code
(Musard Balliu, KTH)

ow level code is challenging: It lacks structure, it uses jumps and symbolic addresses, the control flow is often highly optimized, and registers and memory locations may be reused in ways that make typing extremely challenging. Information flow properties create additional complications: They are hyperproperties relating multiple executions, and the possibility of interrupts and concurrency, and use of devices and features like memory-mapped I/O requires a departure from the usual initial-state final-state account of noninterference. In this work we propose a novel approach to relational verification for machine code. Verification goals are expressed as equivalence of traces decorated with observation points. Relational verification conditions are propagated between observation points using symbolic execution, and discharged using first-order reasoning. We have implemented an automated tool that integrates with SMT solvers to automate the verification task. The tool transforms ARMv7 binaries into an intermediate, architecture-independent format using the BAP toolset by means of a verified translator. We demonstrate the capabilities of the tool on a separation kernel system call handler, which mixes hand-written assembly with gcc-optimized output, a UART device driver and a crypto service modular exponentiation routine.

Informal Seminars Spring 2014

27 Jun 2014 at 13:15 in 4523
Long Proofs of (Seemingly) Simple Formulas
(Mladen Miksa, TCS-KTH)

In 2010, Spence and Van Gelder presented a family of CNF formulas based on combinatorial block designs. They showed empirically that this construction yielded small instances that were orders of magnitude harder for state-of-the-art SAT solvers than other benchmarks of comparable size, but left open the problem of proving theoretical lower bounds. We establish that these formulas are exponentially hard for resolution and even for polynomial calculus, which extends resolution with algebraic reasoning. We also present updated experimental data showing that these formulas are indeed still hard for current CDCL solvers, provided that these solvers do not also reason in terms of cardinality constraints (in which case the formulas can become very easy).
15 May 2014 at 10:00 in room 1537
Towards an understanding of the power of CDCL SAT solvers
(Gustav Sennton, KTH)

The Boolean satisfiability problem (SAT) is the canonical NP-complete problem and hence it seems natural to expect that solving instances of the SAT problem is difficult. However, in practice conflict-driven clause learning (CDCL) SAT solvers do well on many large-scale real-world instances. Therefore it is interesting to study the strengths and weaknesses of CDCL solvers.
CDCL solvers implicitly find resolution proofs for unsatisfiable formulas, but how small are such proofs compared to the smallest possible resolution proof? It was recently shown that CDCL solvers can produce proofs of size at most polynomially longer than the smallest resolution proof. However, these results are non-constructive, i.e. the algorithm is non-deterministic. When it comes to constructive results it was recently shown that, with high probability, the running time of a CDCL solver is polynomial in the size of the smallest corresponding resolution proof as long as the clauses in the resolution proof have constant size (and given certain theoretical assumptions about the CDCL model).
In the first half of this seminar I will go over the resolution proof system, explain how a CDCL solver works, and then give an overview of how to prove guarantees for CDCL performance in terms of resolution. During the second half of the seminar we will look at some of the proofs in more detail.
01 Apr 2014 at 13:00 in 4523
Sound Control Flow Graph Extraction from Incomplete Java Bytecode Programs
(Pedro de Carvalho Gomes, TCS/KTH)

The modular analysis of control flow of incomplete Java bytecode programs is challenging, mainly because of the complex semantics of the language, and the unknown inter-dependencies between the available and unavailable components. In this paper we describe a technique for incremental, modular extraction of control flow graphs that are provably sound w.r.t.~sequences of method invocations and exceptions. The extracted models are suitable for various program analyses, in particular model-checking of temporal control flow safety properties. Soundness comes at the price of over-approximation, potentially giving rise to false positives reports during verification. Still, our technique supports incremental refinement of the already extracted models, as more components code becomes available. The extraction has been implemented as the ConFlEx tool, and test-cases show its utility and efficiency.
The presentation is a rehearsal for the 17th International Conference on Fundamental Approaches to Software Engineering (FASE), one of the European Joint Conferences on Theory and Practice of Software (ETAPS). It is expected to take 25 minutes. After, Pedro will collect feedback for improvement.
19 Mar 2014 at 11:30 in 4523
Inapproximability results for Max-3-Lin-2 and Max-3-Sat
(Jonas Haglund)

This talk will treat two problems in the area of hardness of approximation. An approximation algorithm for an optimization problem always returns a solution that is within some specified distance from the optimal solution. I will cover the main ideas of the inapproximability results for Max-3-Lin-2 and Max-3-Sat. Max-3-Lin-2 is the problem of given an overdetermined system of linear equation in the field of two elements, with exactly three variables in each equation, find an assignment that maximizes the number of satisfied equations. The definition of Max-3-Sat is similar.
I will cover the main ideas in the proofs that both these problems are not possible to approximate in polynomial time, if P != NP, within a factor that is better than the random assignment. Hence these results give boundaries (so-called threshold results) for when it is easy to approximate and when it is hard to approximate Max-3-Lin-2 and Max-3-Sat.
The presentation is based on the paper Some optimal inapproximability results (http://www.nada.kth.se/~johanh/optimalinap.pdf) by Johan Håstad, which gave him his second Gödel prize.
19 Mar 2014 at 11:00 in 4523
Minimum Propositional Proof Length is NP-Hard to Linearly Approximate
(Fredrik Wahlberg)

This presentation will discuss hardness of approximation of minimum lengths of proofs of propositional formulas. In particular, the presentation will focus on linear approximation and the hardness of approximating the minimum length proof within a specified factor for a number of proof systems. These results are obtained by introducing the Monotone Minimum Satisfying Agreement problem and reducing it to the aforementioned approximation problem.
The presentation is based on the article "Minimum Propositional Proof Length is NP-Hard to Linearly Approximate" by M. Alekhnovich, S.R. Buss, S. Moran and T. Pitassi, which is accessible at http://www.math.ucsd.edu/~sbuss/ResearchWeb/kproveApprox/index.html .
19 Mar 2014 at 10:30 in 4523
Short proofs are narrow---resolution made simple
(Gustav Sennton)

It has been quite difficult to prove lower bounds on the size of resolution proofs. The size of a resolution proof is the number of clauses used in the proof. But what if we can use width lower bounds to prove size lower bounds? The width of a resolution proof is the maximum number of literals in any clause in the proof.
In this talk relations between width and size of resolution proofs are presented. The relations basically show that short resolution proofs are narrow, and thus that wide proofs are long, i.e. width lower bounds imply size lower bounds. Furthermore, showing width lower bounds seems a lot simpler than showing size lower bounds. Therefore the presented width-size relations can be used for creating simplified proofs for showing size lower bounds for resolution proofs. During the presentation a general strategy for proving width lower bounds is presented and then used for showing width (and thus size) lower bounds on resolution proofs of an example formula.
The presentation is based on the article "Short proofs are narrow---resolution made simple" by Eli Ben-Sasson and Avi Wigderson (http://dl.acm.org/citation.cfm?doid=375827.375835).
19 Mar 2014 at 10:00 in 4523
Reducing property testing problems to communication complexity
(Max Engardt)

problemDuring 25 minutes I will discuss a method of reducing Property Testing Problems to Communication Complexity problems and also present some new lower bounds for Property Testing Problems using this reduction. These two areas of complexity theory have several similarities (parties with unbounded computational power, limited access to input) but before this method no previous connections between the fields had been made.
Two main topics will be covered: First, the method of the described reduction together with some technical details of the proof will be presented. Secondly, a new lower bound for the problem of testing whether a Boolean function is a parity function on k variables will be discussed. The presentation is based on an article by Eric Blais, Joshua Brody, and Kevin Matulef with the title "Lower Bounds via Communication Complexity, Computational Complexity" which in full can be found at http://dx.doi.org/10.1007/s00037-012-0040-x.
28 Feb 2014 at 13:15 in 4523
From Small Space to Small Width in Resolution
(Mladen Miksa, Theory Group, KTH)

In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. This is a practice talk for STACS '14

Informal Seminars Fall 2013

04 Dec 2013 at 13:15 in room 4523
Cartesian decomposition of n-ary relations: An exercise in fixed point theory
(Dilian Gurov, KTH CSC)

Recently I worked with Minko Markov on the problem of decomposing n-ary relations as the Cartesian product of smaller relations, essentially partitioning the set of attributes of the original relation into pairwise independent sets (intuitively meaning that there is no correlation between the sets of attributes). The problem arose from the domain of verification of software families (where each individual SW product consists of a collection of artefacts) by reusing the verification results as much a possible in order to avoid the individual verification of every single product of the family.
After attacking the problem from different angles we finally found that the story becomes clean and elegant when presenting it in terms of the lattice of attribute partitions, and fixed points of a basic transformation on this lattice. Several of the definitions and theorems we had worked out became redundant, due to the well-known Knaster-Tarski fixed point theorem for lattices. In particular, the theorem guarantees the existence of a least fixed point for monotone transformers (eliminating the need to define separately what we are looking for, namely a maximal decomposition), and gives an iterative construction to compute this fixed point (by starting from the bottom of the lattice and iteratively applying the transformer until stabilization).
I believe the talk to be of instructional (and aesthetic) value to graduate students that want to learn a bit about fixed points in computer science. I plan to give the talk following the above "story", and using the white board only.
22 Oct 2013 at 15:00 in room 1625
Efficient and Fully Abstract Routing of Futures in Object Network Overlays
(Karl Palmskog, KTH CSC)

In distributed object systems, it is desirable to enable migration of objects between locations, e.g., in order to support efficient resource allocation. Existing approaches build complex routing infrastructures to handle object-to-object communication, typically on top of IP, using, e.g., message forwarding chains or centralized object location servers. These solutions are costly and problematic in terms of efficiency, overhead, and correctness. We show how location independent routing can be used to implement object overlays with complex messaging behavior in a sound, fully abstract, and efficient way, on top of an abstract network of processing nodes connected point-to-point by asynchronous channels. We consider a distributed object language with futures, essentially lazy return values. Futures are challenging in this context due to the global consistency requirements they impose. The key conclusion is that execution in a decentralized, asynchronous network can preserve the standard, network-oblivious behavior of objects with futures, in the sense of contextual equivalence. To the best of our knowledge, this is the first such result in the literature. We also believe the proposed execution model may be of interest in its own right in the context of large-scale distributed computing.
15 Oct 2013 at 14:00 in room 4523
A Logic for Information Flow Analysis of Distributed Programs
(Musard Balliu, KTH CSC)

Securing communication in large scale distributed systems is an open problem. When multiple principals exchange sensitive information over a network, security and privacy issues arise immediately. For instance, in an online auction system we may want to ensure that no bidder knows the bids of any other bidder before the auction is closed. Such systems are typically interactive/reactive and communication is mostly asynchronous, lossy or unordered. Language-based security provides language mechanisms for enforcing end-to-end security. However, with few exceptions, previous research has mainly focused on relational or synchronous models, which are generally not suitable for distributed systems.
This paper proposes a general knowledge-based account of possibilistic security from a language perspective and shows how existing trace-based conditions fit in. A syntactic characterization of these conditions, given by an epistemic temporal logic, shows that existing model checking tools can be used to enforce security.
This is a rehearsal of my presentation at NordSec 2013.

Informal Seminars Spring 2013

05 Jun 2013 at 16:00 in room 1537
Resource Protection using Atomics: Patterns and Verifications
(Afshin Amighi, University of Twente)

Modular reasoning about non-blocking concurrent data structures is crucial to establish the correctness of concurrent applications. To achieve this, specifications of the synchronization mechanisms used by these non-blocking concurrent classes to prevent concurrent access to shared data, are essential. This talk presents an approach to specifying such lock-free synchronization mechanisms in terms of the thread’s role and permissions. The approach is formalized in a specification for the AtomicInteger class from the java.util.concurrent library, using abstract predicates and permission-based concurrent Separation Logic. The specification is set up to capture different synchronization patterns, both cooperative and competitive. We illustrate the use of the patterns in three case studies, where for each case study we verify that it indeed correctly synchronizes access to the protected data.

Informal Seminars Fall 2012

10 Dec 2012 at 13:15 in room 4523
Motion Planning and Revision under Linear Temporal Logic Specifications
(Meng Guo and Dimos Dimarogonas, KTH EE)

We present a temporal logic based motion planning approach for an autonomous robotic agent. An automaton-based model checking algorithm is used to synthesize a discrete plan satisfying a given task specification. Then a hybrid controller that implements the discrete plan is constructed. We will also discuss about how to deal with uncertainties in the environment, and how to revise the task specification if it can not be achieved (for the agent within this workspace).
22 Oct 2012 at 13:15 in room 4523
PolderCast: Fast, Robust, and Scalable Architecture for P2P Topic-based Pub/Sub
(Vinay Setty, University of Oslo)

We propose PolderCast, a P2P topic-based publish/subscribe system that is (a) fault-tolerant and robust, (b) scalable wrt the number of nodes interested in a topic and number of topics that nodes are interested in, and (c) fast in terms of dissemination latency while (d) attaining a low communication overhead. This combination of properties is provided by an implementation that blends deterministic propagation over maintained rings with probabilistic dissemination following a limited number of random shortcuts. The rings are constructed and maintained using gossiping techniques. The random shortcuts are provided by two distinct peer-sampling services: Cyclon generates purely random links while Vicinity produces interest-induced random links.
We analyze PolderCast and survey it in the context of existing approaches. We evaluate PolderCast experimentally using real-world workloads from Twitter and Facebook traces. We use Scribe [1] as a baseline in a number of experiments. Robustness with respect to churn is evaluated through traces from the Skype super-peer network. We show that the experimental results corroborate all of the above properties in settings of up to 10K nodes, 10K topics, and 5K topics per-node.
This is a rehearsal talk for Middleware 2012.
09 Oct 2012 at 15:15 in 4523
TreeDroid: A Tree Automaton Based Approach to Enforcing Data Processing Policies
(Andreas Lundblad, KTH CSC)

Current monitoring techniques handle linear control flow constraints such as "'runQuery' may be evaluated only after 'sanitize'". In practice however, many policies require the possibility to capture data flow aspects as well. An example is a policy stating that "arguments to the function 'runQuery' must be either constants, outputs of a function 'sanitize', or concatenations of any such values".
We present a novel approach to security policy monitoring that uses tree automata to capture constraints on the way data is processed along an execution. We present a lambda-calculus based model of the framework, investigate some of the models meta-properties, and show how it can be implemented using labels corresponding to automaton states to reflect the computational histories of each data item. Finally an implementation targeting Android's Dalvik VM is presented together with an evaluation regarding functionality and performance on five real world case studies.
The talk is a rehearsal for CCS'12.
24 Sep 2012 at 13:15 in room 1537
Sound Control-Flow Graph Extraction for Java Programs with Exceptions
(Pedro de Carvalho Gomes, KTH CSC)

We present an algorithm to extract control-flow graphs from Java bytecode, considering exceptional flows. We then establish its correctness: the behavior of the extracted graphs is shown to be a sound over-approximation of the behavior of the original programs. Thus, any temporal safety property that holds for the extracted control-flow graph also holds for the original program.This makes the extracted graphs suitable for performing various static analyses, in particular model checking. The extraction proceeds in two phases First, we translate Java bytecode into BIR, a stack-less intermediate representation. The BIR transformation is developed as a module of Sawja, a novel static analysis framework for Java bytecode. Besides Sawja's efficiency, the resulting intermediate representation is more compact than the original bytecode and provides an explicit representation of exceptions. These features make BIR a natural starting point for sound control-flow graph extraction. Next, we formally define the transformation from BIR to control-flow graphs, which (among other features) considers the propagation of uncaught exceptions within method calls. We prove the correctness of the two-phase extraction by suitably combining the properties of the two transformations with those of an idealized control-flow graph extraction algorithm, whose correctness has been proved directly. The control-flow graph extraction algorithm is implemented in the ConFlEx tool. A number of test-cases show the efficiency and the utility of the implementation, and paves the ground for a fully-modular extraction algorithm.
The talk is a rehearsal for the 10th International Conference on Software Engineering and Formal Methods (SEFM'12).

Informal Seminars Spring 2012

28 May 2012 at 13:15 in room 1625
ENCOVER: Symbolic Exploration for Information Flow Security
(Musard Balliu, KTH CSC)

We address the problem of program verification for information flow policies by means of symbolic execution and model checking. Noninterference-like security policies are formalized using epistemic logic. We show how the policies can be accurately verified using a combination of concolic testing and SMT solving. As we demonstrate, many scenarios considered tricky in the literature can be solved precisely using the proposed approach. This is confirmed by experiments performed with ENCOVER, a tool based on Java PathFinder and Z3, which we have developed for epistemic noninterference concolic verification.
This is a rehearsal talk for CSF 2012, based on joint work with Mads Dam and Gurvan Le Guernic.
22 Feb 2012 at 15:00 in room 1537
A two prover one round game with strong soundness
(Michail Lampis, KTH CSC)

We discuss the paper "A two prover one round game with strong soundness" by Subash Khot and Mulli Safra from FOCS 2011.

Informal Seminars Fall 2011

09 Nov 2011 at 13:15 in room 1537
ProMoVer: Modular Verification of Temporal Safety Properties
(Siavash Soleimanifard, KTH CSC)

In this talk, I will introduce ProMoVer, a tool 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 at the procedure-level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations, and is based here on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre- and post-processing. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light-weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. I evaluate the tool on a number of applications from the smart card domain.
This is a rehearsal talk for SEFM'11.
11 Oct 2011 at 10:15 in room 4523
Approximating Graphic TSP by Matchings
(Tobias Moemke, KTH CSC)

We present a framework for approximating the metric TSP based on a novel use of matchings. Traditionally, matchings have been used to add edges in order to make a given graph Eulerian, whereas our approach also allows for the removal of certain edges leading to a decreased cost.
For the TSP on graphic metrics (graph-TSP), the approach yields a 1.461-approximation algorithm with respect to the Held-Karp lower bound. For graph-TSP restricted to a class of graphs that contains degree three bounded and claw-free graphs, we show that the integrality gap of the Held-Karp relaxation matches the conjectured ratio 4/3. The framework allows for generalizations in a natural way and also leads to a 1.586-approximation algorithm for the traveling salesman path problem on graphic metrics where the start and end vertices are prespecified.
This is a rehearsal talk for FOCS.
03 Oct 2011 at 13:15 in room 1439
Provably Correct Control-Flow Graphs from Java Programs with Exceptions
(Pedro de Carvalho Gomes, KTH CSC)

We present an algorithm to extract flow graphs from Java bytecode, focusing on exceptional control flows. We prove its correctness, meaning that the behaviour of the extracted control-flow graph is an over-approximation of the behaviour of the original program. Thus any safety property that holds for the extracted control-flow graph also holds for the original program. This makes control-flow graphs suitable for performing different static analyses.
For precision and efficiency, the extraction is performed in two phases. In the first phase the program is transformed into a BIR program, where BIR is a stack-less intermediate representation of Java bytecode; in the second phase the control-flow graph is extracted from the BIR representation. To prove the correctness of the two-phase extraction, we also define a direct extraction algorithm, whose correctness can be proven immediately. Then we show that the behaviour of the control-flow graph extracted via the intermediate representation is an over-approximation of the behaviour of the directly extracted graphs, and thus of the original program.
This is a rehearsal talk for Foveoos 2011 (http://foveoos2011.cost-ic0701.org/) and feedback is very welcome.
27 Sep 2011 at 13:15 in room 1537
Boolean polynomials and Gröbner bases: An Algebraic Approach to solving the SAT-problem
(John Sass, SU)

In this seminar we will discuss a method for solving the SAT-problem based on abstract algebra. The first step of the method is to convert the boolean formula to a set of \mathbb{Z}_2-polynomials, and looking at the ideal generated by these polynomials. If this ideal coincides with the entire polynomial ring, then and only then is the original boolean formula unsatisfiable, and we determine if this is the case by looking at a Gröbner basis for this ideal. Such a basis can be found using the Buchberger algorithm, which in the general case is a double exponential time algorithm.
The seminar will be split into two 45-minute segments, with a ten minute break in between. In the first half of the seminar we will discuss the general method, including an introduction to multivariate polynomial reduction, Gröbner bases and the Buchberger algorithm. In the second half we will discuss the technical details, as well as implementation tricks and heuristic suggestions for the Buchberger algorithm which turn it into an exponential time algorithm. If there is time, we will also discuss how the method can be generalised and developed further.
29 Aug 2011 at 13:15 in room 1537
Canonizable Partial Order Generators
(Mateus de Oliveira Oliveira, KTH CSC)

In a previous work we introduced slice graphs as a way to specify both infinite languages of directed acyclic graphs (DAGs) and infinite languages of partial orders. Therein we focused on the study of Hasse diagram generators, i.e., slice graphs that generate only transitive reduced DAGs, and showed that they could be used to solve several problems related to the partial order behavior of p/t-nets. In the present work we show that both slice graphs and Hasse diagram generators are worth studying on their own. First, we prove that any slice graph SG can be effectively transformed into a Hasse diagram generator HG representing the same set of partial orders. Thus from an algorithmic standpoint we introduce a method of transitive reducing infinite families of DAGs specified by slice graphs. Second, we identify the class of saturated slice graphs. By using our transitive reduction algorithm, we prove that the class of partial order languages representable by saturated slice graphs is closed under union, intersection and even under a suitable notion of complementation (cut-width complementation). Furthermore partial order languages belonging to this class can be tested for inclusion and admit canonical representatives in terms of Hasse diagram generators. As an application of our results, we give stronger forms of some results in our previous work, and establish some unknown connections between the partial order behavior of $p/t$-nets and other well known formalisms for the specification of infinite families of partial orders, such as Mazurkiewicz trace languages and message sequence chart (MSC) languages.

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.

Doktorandseminarier höstterminen 2010 / Seminars Held Fall 2010

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.

Doktorandseminarier vårterminen 2010 / Seminars Held Spring 2010

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

Avklarade doktorandseminarier vårterminen 2009 / Seminars Held Spring 2009

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.

Avklarade doktorandseminarier vårterminen 2008 / Seminars Held Spring Term 2008

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.

Avklarade doktorandseminarier höstterminen 2007 / Seminars Held Autumn Term 2007

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.

Avklarade doktorandseminarier vårterminen 2007 / Seminars Held Spring Term 2007

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.