Abstract: 
This dissertation focuses on algorithmic aspects of program verification, and presents modeling and complexity advances on several problems related to the
static analysis of programs, the stateless model checking of concurrent programs, and the competitive analysis of realtime scheduling algorithms.
Our contributions can be broadly grouped into five categories.
Our first contribution is a set of new algorithms and data structures for the quantitative and dataflow analysis of programs, based on the graphtheoretic notion of treewidth.
It has been observed that the controlflow graphs of typical programs have special structure, and are characterized as graphs of small treewidth.
We utilize this structural property to provide faster algorithms for the quantitative and dataflow analysis of recursive and concurrent programs.
In most cases we make an algebraic treatment of the considered problem,
where several interesting analyses, such as the reachability, shortest path, and certain kind of dataflow analysis problems follow as special cases.
We exploit the constanttreewidth property to obtain algorithmic improvements for ondemand versions of the problems,
and provide data structures with various tradeoffs between the resources spent in the preprocessing and querying phase.
We also improve on the algorithmic complexity of quantitative problems outside the algebraic path framework,
namely of the minimum meanpayoff, minimum ratio, and minimum initial credit for energy problems.
Our second contribution is a set of algorithms for Dyck reachability with applications to datadependence analysis and alias analysis.
In particular, we develop an optimal algorithm for Dyck reachability on bidirected graphs, which are ubiquitous in contextinsensitive, fieldsensitive pointsto analysis.
Additionally, we develop an efficient algorithm for contextsensitive datadependence analysis via Dyck reachability,
where the task is to obtain analysis summaries of library code in the presence of callbacks.
Our algorithm preprocesses libraries in almost linear time, after which the contribution of the library in the complexity of the client analysis is (i)~linear in the number of call sites and (ii)~only logarithmic in the size of the whole library, as opposed to linear in the size of the whole library.
Finally, we prove that Dyck reachability is Boolean Matrix Multiplicationhard in general, and the hardness also holds for graphs of constant treewidth.
This hardness result strongly indicates that there exist no combinatorial algorithms for Dyck reachability with truly subcubic complexity.
Our third contribution is the formalization and algorithmic treatment of the Quantitative Interprocedural Analysis framework.
In this framework, the transitions of a recursive program are annotated as good, bad or neutral, and receive a weight which measures
the magnitude of their respective effect.
The Quantitative Interprocedural Analysis problem asks to determine whether there exists an infinite run of the program where the longrun ratio of the bad weights over the good weights is above a given threshold.
We illustrate how several quantitative problems related to static analysis of recursive programs can be instantiated in this framework,
and present some case studies to this direction.
Our fourth contribution is a new dynamic partialorder reduction for the stateless model checking of concurrent programs. Traditional approaches rely on the standard Mazurkiewicz equivalence between traces, by means of partitioning the trace space into equivalence classes, and attempting to explore a few representatives from each class.
We present a new dynamic partialorder reduction method called the Datacentric Partial Order Reduction (DCDPOR).
Our algorithm is based on a new equivalence between traces, called the observation equivalence.
DCDPOR explores a coarser partitioning of the trace space than any exploration method based on the standard Mazurkiewicz equivalence.
Depending on the program, the new partitioning can be even exponentially coarser.
Additionally, DCDPOR spends only polynomial time in each explored class.
Our fifth contribution is the use of automata and gametheoretic verification techniques in the competitive analysis and synthesis of realtime scheduling algorithms for firmdeadline tasks.
On the analysis side, we leverage automata on infinite words to compute the competitive ratio of realtime schedulers subject to various environmental constraints.
On the synthesis side, we introduce a new instance of twoplayer meanpayoff partialinformation games, and show
how the synthesis of an optimal realtime scheduler can be reduced to computing winning strategies in this new type of games.

Notes: 
First, I am thankful to my advisor, Krishnendu Chatterjee, for offering me the opportunity to
materialize my scientific curiosity in a remarkably wide range of interesting topics, as well as for his constant availability and continuous support throughout my doctoral studies. I have had the privilege of collaborating with, discussing and getting inspired by all members of my committee: Thomas A. Henzinger, Ulrich Schmid and Martin A. Nowak. The role of the above four people has been very instrumental both to the research carried out for this dissertation, and to the researcher I evolved to in the process.
I have greatly enjoyed my numerous brainstorming sessions with Rasmus IbsenJensen, many
of which led to results on lowtreewidth graphs presented here. I thank Alex Kößler for our
discussions on modeling and analyzing realtime scheduling algorithms, Yaron Velner for our
collaboration on the Quantitative Interprocedural Analysis framework, and Nishant Sinha for our initial discussions on partial order reduction techniques in stateless model checking. I also thank Jan Otop, Ben Adlam, Bernhard Kragl and Josef Tkadlec for our fruitful collaborations on
topics outside the scope of this dissertation, as well as the interns Prateesh Goyal, Amir Kafshdar Goharshady, Samarth Mishra, Bhavya Choudhary and Marek Chalupa, with whom I have shared my excitement on various research topics. Together with my collaborators, I thank officemates and members of the Chatterjee and Henzinger groups throughout the years, Thorsten Tarrach, Ventsi Chonev, Roopsha Samanta, Przemek Daca, Mirco Giacobbe, Tanja Petrov, Ashutosh
Gupta, Arjun Radhakrishna, Petr Novontý, Christian Hilbe, Jakob Ruess, Martin Chmelik,
Cezara Dragoi, Johannes Reiter, Andrey Kupriyanov, Guy Avni, Sasha Rubin, Jessica Davies, Hongfei Fu, Thomas Ferrère, Pavol Cerný, Ali Sezgin, Jan Kretínský, Sergiy Bogomolov, Hui
Kong, Benjamin Aminof, DucHiep Chu, and Damien Zufferey. Besides collaborations and office spaces, with many of the above people I have been fortunate to share numerous whiteboard
discussions, as well as memorable long walks and amicable meals accompanied by stimulating
conversations. I am highly indebted to Elisabeth Hacker for her continuous assistance in matters
that often exceeded her official duties, and who made my integration in Austria a smooth process.
