Reactive Synthesis
Reactive synthesis is the problem of turning a temporal logic specification into a reactive system. A major advantage of synthesis over verification is that manual programming is no longer required: synthesis automatically derives an implementation that is correct by construction. After synthesis was defined as an automated reasoning problem, it had long been considered infeasible for any interesting application. Recent years have brought advances both in reasoning methods that can be used as tools in the synthesis process, and in synthesis approaches themselves. As a result, case studies of substantial size can now be synthesized automatically.

In this lecture, we will formally define the synthesis problem and look at basic (game-based) approaches to solve it. As these approaches suffer from a state explosion problem that makes synthesis infeasible for all but very simple specifications, we will go on to review specialized techniques (GR(1)-synthesis, lazy synthesis, parameterized synthesis) that try to circumvent this problem in different ways.

Automated reasoning for first-order logic: theory, practice and challenges
Automated reasoning for first-order logic has a wide range of applications in verification, knowledge representation and proving mathematical theorems. First-order logic provides flexible expressive formalism for specifying problems in different domains. During the last 50 years there has been a large amount of research aimed at developing efficient reasoning methods for first-order logic. This lead to new logical calculi, frameworks for establishing completeness of such calculi, methods for redundancy elimination and advanced implementation techniques. In these lectures we take a journey from theoretical foundations of automated reasoning for first-order logic to practical implementation techniques, applications and discuss current challenges.

Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems
Model-driven development has been proposed as a way to deal with the increasing complexity of real-time and embedded systems, while reducing the time and cost to market. The use of models should permit early assessment of the functional correctness of a given design as well as requirements for resources (e.g. energy, memory, and bandwidth) and real-time and performance guarantees.

During these lectures we will offer a thorough account of the formalism of timed automata due Alur and Dill as well as several recent extensions. These extensions include priced timed automa- ta, (priced) timed games and most recently stochastic timed automata and we will introduce a number of associated decision problems related to model-checking, refinement checking and optimal scheduling and synthesis. The frontier of decidability will be drawn including pointing out a number of open problems.

The lectures will also emphasize the substantial research effort in the design of algorithms and datastructures for efficient analysis of timed automata and its extensions covering important datastructures such as DBMs (difference bounded matrices) and CDD (clock difference diagrams) as to be found in the verification tool UPPAAL and its various branches. Also, substantial focus will be on the application of statistical model checking where properties are settled up to user- specied level of confidence based on randomly generated simulation runs. A number of industrial applications will also be given.

Mechanized semantics with applications to program proof and compiler verification
The goal of this lecture is to show how modern theorem provers -- I use the Coq proof assistant -- can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs as well as over generic program transformations, as typically found in compilers.

The topics covered include:

• Operational semantics: small-step, big-step, definitional interpreters.
• Some forms of denotational semantics.
• Axiomatic semantics and Hoare logic.
• Generation of verification conditions; application to program proof.
• Compilation to virtual machine code and its proof of correctness.
• An example of an optimizing program transformation and its proof of correctness.

Answer Set Solving in Practice
Answer Set Programming (ASP) provides a declarative tool for modeling various problems typical to Knowledge Representation and Reasoning in particular and AI in general.
The unique pairing of declarativeness and performance allows for concentrating on an actual problem, rather than a smart way of implementing it. The ASP approach is not only highly suitable for the practitioner solving an AI problem at hand but also for disseminating many basic AI techniques through teaching their (executable) formalization in ASP.

The potential target audience for the tutorial is thus manifold, and comprises graduate students in AI, teachers of AI at universities, researchers addressing NP or NP^NP hard problems, as well as Industrials addressing NP or NP^NP hard problems.

What makes this tutorial different from others on ASP is its focus on putting ASP at work.
This comprises a good understanding of ASP solving technology and systems as well as basic skills in ASP's modeling capacities.

Contents:
The tutorial aims at acquainting the participant with ASP's modeling and solving methodology, enabling her/him to independent problem solving using ASP systems.
To this end, the tutorial starts with an introduction to the essential formal concepts of ASP, needed for understanding its semantics and solving technology. In fact, ASP solving rests on two major components: A grounder turning specifications in ASP's modeling language into propositional logic programs and a solver computing a requested number of answer sets of the given program.
Building on the aforementioned formal concepts, we provide a characterization of ASP's inference schemes that are in turn mapped into algorithms relying on advanced Boolean Constraint technology. We illustrate this technology through the ASP solver \texttt{clasp}, developed at the University of Potsdam, and winning first places at international ASP, CASC, MISC, PB, and SAT competitions. Similarly, ASP's grounding inferences are discussed in conjunction with (deductive) database techniques.
The remainder of the tutorial is dedicated to applying ASP, involving an introduction to ASP's modeling language, its solving methodology, and advanced techniques fostering scalability. The latter is illustrated via some real-world applications, taken from bio-informatics.
All involved ASP systems are freely available from http://potassco.sourceforge.net.