Ph.D. Program

Basic notions of algorithms and complexity; Divide-and-Conquer; Dynamic Programming; Basic data structures: heaps, hash tables; Greedy; Local Search; Network Flow; All-pairs Shortest Paths; NP-complete problems and intractability; PSPACE

Basics on formal models of computations, operational semantics and (labelled) transition systems, formal languages, preliminary notions of process algebraic approaches. Preliminary concepts of software verification, typical verification flow, common program analysis techniques, decision procedures. Basic concepts of software modelling and analysis with stochastic processes, discrete-time markov processes, and petri nets.

Basic concepts of software development paradigms, application domains, the software life cycle, design of software systems and modeling, software architectures. The course also provide some basic knowledge of the tools used to generate software programs from models.

How to write a paper. How to give a scientific talk. How to referee a scientific paper.

This course analyses different kind of analysis for software: static, dynamic and hybrid. Introduce the theoretical principles of static analysis and present some of the approaches and tools used in software practice.

General concepts and techniques of software testing. Main approaches for dependability and security validation. Most interesting research challenges in software testing.

This course will introduce students to the theory, and to tools and methods for domain-specific modelling and for probabilistic model checking. The first part of the course will cover stochastic modelling using the Prism probabilistic model checker, as well as the basics of quantitative verification of system properties employing probabilistic temporal logics like PCTL and CSL. The second part of the module will introduce object-oriented domain-specific language development using the Eclipse Modelling Framework, graphical syntax specification using the Eclipse Graphical Modeling Framework and Eugenai, and programmatic model management using the Eclipse Epsilon family of languages.

Modelling of reactive systems, review of the model checking approach, temporal logics (LTL, CTL, and CTL*), safety and liveness properties of reactive systems, fairness conditions.

Modelling, Analysis, and Testing of Probabilistic Systems: Stochastic Process Algebras, Markov Decision Processes, Timed Automata, Queueing Networks

Principles of Parallel and Concurrent Programming, Introduction to Concurrency, Paradigms for Parallel Programming, Interference and Atomicity, Mutual Exclusion, Semaphores, Monitors, Elements of Distributed Programming, Concurrent Programming Languages

Introduction to linear programming; the set cover problem; greedy algorithms and local search; rounding data and dynamic programming; deterministic rounding of linear programs; random sampling and randomized rounding of linear programs; the primal-dual method; techniques to prove the hardness of approximation

Algorithmic Game Theory (Equilibria: dominant versus Nash equilibria; Computational issues of equilibria); Congestion Games; Mechanism design; Computational social choice

Basics in probability theory; coupon collector and contention resolution; Yao’s principle and the secretary problem; the probabilistic method; randomized min-cut and quicksort; Chernoff bounds; random graphs; smoothed analysis

Multi-Agent Systems and Simulations

Parameterized Complexity