@string{brics = "{BRICS}"}
@string{daimi = "Department of Computer Science, University of Aarhus"}
@string{iesd = "Department of Computer Science, Institute
of Electronic Systems, Aalborg University"}
@string{rs = "Research Series"}
@string{ns = "Notes Series"}
@string{ls = "Lecture Series"}
@string{ds = "Dissertation Series"}
@techreport{BRICS-DS-02-5,
author = "Pagh, Rasmus",
title = "Hashing, Randomness and Dictionaries",
institution = brics,
year = 2002,
type = ds,
number = "DS-02-5",
address = daimi,
month = oct,
note = "PhD thesis. x+167~pp",
comment = "Defence: October~11, 2002",
abstract = "This thesis is centered around one of the most
basic information retrieval problems, namely
that of storing and accessing the elements of a
set. Each element in the set has some
associated information that is returned along
with it. The problem is referred to as the {\em
dictionary\/} problem, due to the similarity to
a bookshelf dictionary, which contains a set of
words and has an explanation associated with
each word. In the {\em static\/} version of the
problem the set is fixed, whereas in the {\em
dynamic\/} version, insertions and deletions of
elements are possible.\bibpar
The approach taken is that of the theoretical
algorithms community. We work (almost)
exclusively with a {\em model}, a mathematical
object that is meant to capture essential
aspects of a real computer. The main model
considered here (and in most of the literature
on dictionaries) is a unit cost RAM with a word
size that allows a set element to be stored in
one word.\bibpar
We consider several variants of the dictionary
problem, as well as some related problems. The
problems are studied mainly from an upper bound
perspective, i.e., we try to come up with
algorithms that are as efficient as possible
with respect to various computing resources,
mainly computation time and memory space. To
some extent we also consider lower bounds,
i.e., we attempt to show limitations on how
efficient algorithms are possible. A central
theme in the thesis is {\em randomness}.
Randomized algorithms play an important role,
in particular through the key technique of {\em
hashing}. Additionally, probabilistic methods
are used in several proofs.",
linkhtmlabs = "",
linkpdf = "",
linkps = ""
}
@techreport{BRICS-DS-02-4,
author = "M{\o}ller, Anders",
title = "Program Verification with Monadic Second-Order
Logic \& Languages for {W}eb Service
Development",
institution = brics,
year = 2002,
type = ds,
number = "DS-02-4",
address = daimi,
month = sep,
note = "PhD thesis. xvi+337~pp",
comment = "Defence: September~9, 2002",
abstract = "Domain-specific formal languages are an
essential part of computer science, combining
theory and practice. Such languages are
characterized by being tailor-made for specific
application domains and thereby providing
expressiveness on high abstraction levels and
allowing specialized analysis and verification
techniques. This dissertation describes two
projects, each exploring one particular
instance of such languages: monadic
second-order logic and its application to
program verification, and programming languages
for construction of interactive Web services.
Both program verification and Web service
development are areas of programming language
research that have received increased attention
during the last years.\bibpar
We first show how the logic Weak monadic
Second-order Logic on Strings and Trees can be
implemented efficiently despite an intractable
theoretical worst-case complexity. Among
several other applications, this implementation
forms the basis of a verification technique for
imperative programs that perform data-type
operations using pointers. To achieve this, the
basic logic is extended with layers of language
abstractions. Also, a language for expressing
data structures and operations along with
correctness specifications is designed. Using
Hoare logic, programs are split into loop-free
fragments which can be encoded in the logic.
The technique is described for recursive data
types and later extended to the whole class of
graph types. As an example application, we
verify correctness properties of an
implementation of the insert procedure for
red-black search trees.\bibpar
We then show how Web service development can
benefit from high-level language support.
Existing programming languages for Web services
are typically general-purpose languages that
provide only low-level primitives for common
problems, such as maintaining session state and
dynamically producing HTML or XML documents. By
introducing explicit language-based mechanisms
for those issues, we liberate the Web service
programmer from the tedious and error-prone
alternatives. Specialized program analyses aid
the programmer by verifying at compile time
that only valid HTML documents are ever shown
to the clients at runtime and that the
documents are constructed consistently. In
addition, the language design provides support
for declarative form-field validation, caching
of dynamic documents, concurrency control based
on temporal-logic specifications, and
syntax-level macros for making additional
language extensions. In its newest version, the
programming language is designed as an
extension of Java. To describe classes of XML
documents, we introduce a novel XML schema
language aiming to both simplify and generalize
existing proposals. All parts are implemented
and tested in practice.\bibpar
Both projects involve design of high-level
languages and specialized analysis and
verification techniques, supporting the thesis
that the domain-specific paradigm can provide a
versatile and productive approach to
development of formal languages"
}
@techreport{BRICS-DS-02-3,
author = "Jacob, Riko",
title = "Dynamic Planar Convex hull",
institution = brics,
year = 2002,
type = ds,
number = "DS-02-3",
address = daimi,
month = may,
note = "PhD thesis. xiv+112~pp",
comment = "Defence: May~31, 2002",
abstract = "We determine the computational complexity of
the dynamic convex hull problem in the planar
case. We present a data structure that
maintains a finite set of points in the plane
under insertion and deletion of points in
amortized $O(\log n)$ time. Here n denotes the
number of points in the set. The data structure
supports the reporting of the extreme point of
the set in some direction in worst-case and
amortized $O(\log n)$ time. The space usage of
the data structure is $O(n)$. We give a lower
bound on the amortized asymptotic time
complexity that matches the performance of this
data structure",
linkhtmlabs = "",
linkpdf = "",
linkps = ""
}
@techreport{BRICS-DS-02-2,
author = "Dantchev, Stefan",
title = "On Resolution Complexity of Matching
Principles",
institution = brics,
year = 2002,
type = ds,
number = "DS-02-2",
address = daimi,
month = may,
note = "PhD thesis. xii+70~pp",
comment = "Defence: May~10, 2002",
abstract = "Studying the complexity of mathematical proofs
is important not only for automated theorem
proving, but also for Mathematics as a whole.
Each significant result in this direction would
potentially have a great impact on Foundations
of mathematics.\bibpar
Surprisingly enough, the general Proof
Complexity is closely related to Propositional
Proof Complexity. The latter area was founded
by Cook and Reckhow in 1979, and enjoyed quite
a fast development since then. One of the main
research directions is finding the precise
complexity of some natural combinatorial
principle within a relatively weak
propositional proof system. The results in the
thesis fall in this category. We study the
Resolution complexity of some Matching
Principles. The three major contributions of
the thesis are as follows.\bibpar
Firstly, we develop a general technique of
proving resolution lower bounds for the perfect
matchingprinciples based on regular planar
graphs. No lower bounds for these were known
prior to our work. As a matter of fact, one
such problem, the Mutilated Chessboard, was
suggested as hard to automated theorem provers
in 1964, and remained open since then. Our
technique proves a tight resolution lower bound
for the Mutilated Chessboard as well as for
Tseitin tautologies based on rectangular grid
graph. We reduce these problems to Tiling
games, a concept introduced by us, which may be
of interest on its own.\bibpar
Secondly, we find the exact Tree-Resolution
complexity of the Weak Pigeon-Hole Principle.
It is the most studied combinatorial principle,
but even its Tree-Resolution complexity was
unknown prior to our work. We develop a new,
more general method for proving Tree-Resolution
lower bounds. We also define and prove
non-trivial upper bounds on worst-case proofs
of the Weak Pigeon-Hole Principle. The
worst-case proofs are first introduced by us,
as a concept opposite to the optimal
proofs.\bibpar
Thirdly, we prove Resolution width-size
trade-offs for the Pigeon-Hole Principle.
Proving the size lower bounds via the width
lower bounds was known since the seminal paper
of Haken, who first proved an exponential lower
bound for the ordinary Pigeon-Hole Principle.
The width-size trade-offs however were not
studied at all prior to our work. Our result
gives an optimal width-size trade-off for
resolution in general"
}
@techreport{BRICS-DS-02-1,
author = "M{\"o}ller, M. Oliver",
title = "Structure and Hierarchy in Real-Time Systems",
institution = brics,
year = 2002,
type = ds,
number = "DS-02-1",
address = daimi,
month = apr,
note = "PhD thesis. xvi+228~pp",
abstract = "The development of digital systems is
particularly challenging, if their correctness
depends on the right timing of operations. One
approach to enhance the reliability of such
systems is model-based development. This allows
for a formal analysis throughout all stages of
design.\bibpar
Model-based development is hindered mainly by
the lack of adequate modeling languages and the
high computational cost of the analysis. In
this thesis we improve the situation along both
axes.\bibpar
First, we bring the mathematical model closer
to the human designer. This we achieve by
casting hierarchical structures---as known from
statechart-like formalisms---into a formal
timed model. This shapes a high-level language,
which allows for fully automated
verification.\bibpar
Second, we use sound approximations to achieve
more efficient automation in the verification
of timed properties. We present two novel
state-based techniques that have the potential
to reduce time and memory consumption
drastically.\bibpar
The first technique makes use of structural
information, in particular loops, to exploit
regularities in the reachable state space. Via
shortcut-like additions to the model we avoid
repetition of similar states during an
exhaustive state space exploration.\bibpar
The second technique applies the abstract
interpretation framework to a real-time
setting. We preserve the control structure and
approximate only the more expensive time
component of a state. The verification of
infinite behavior, also known as liveness
properties, requires an assumption on the
progress of time. We incorporate this
assumption by means of limiting the behavior of
the model with respect to delay steps. For a
next-free temporal logic, this modification
does not change the set of valid
properties.\bibpar
We supplement our research with experimental
run-time data. This data is gathered via
prototype implementations on top of the model
checking tools UPPAAL and MOCHA",
linkhtmlabs = "",
linkpdf = ""
}