 Graduate Seminars
|
Informal PhD Student Seminars in Theoretical Computer Science
The PhD student seminars are intended to be informal and relaxed
without the "polish" of the official seminars. The seminars can
discuss for example recent results (your own or from an article)
or survey some interesting topic. The intended audience is primarily
PhD students, but everyone is welcome. Contact
Björn Terelius
if you want to give a seminar or receive email announcements about
upcoming seminars.
More information about
practical details
are available in Swedish. There is also a page with
previous seminars.
See also the page with the TCS groups
official seminars.
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.
|