SAT and SMT: Theory and Practice
In the past decade, there has been a steady increase in the use of formal methods to verify systems. This success is largely due to advances in algorithms for Boolean logic. In particular, fast algorithms for Boolean satisfiability (SAT) have increased the capability of core Boolean verification engines by several orders of magnitude.

While Boolean methods are capable of modeling most verification tasks, systems are usually designed and modeled at a higher level, and the translation to Boolean logic can be both expensive and obfuscating. Satisfiability Modulo Theories (SMT) is the natural next step in the evolution of fast and automatic verification engines. Built on top of fast SAT solvers, SMT solvers can match the speed and automation of today's Boolean engines while at the same time providing high-level reasoning capabilities that give them a significant advantage in both ease of use and performance.

In these lectures, I will present a theoretical framework for SAT and SMT, discuss the history and content of the main innovations that have led to important performance improvements, and give some perspective on how to build and use SAT and SMT solvers.

Formal Methods for Software Correctness and Security
Reliability and security of executable code is an important concern in many application domains, and in particular mobile code where code consumers run code that originate from untrusted and potentially malicious producers. The purpose of this course is to introduce some static mechanisms to ensure properties of source programs, and to demonstrate how the evidence they provide may be transferred to their executable counterparts, in the form of a certificate that can be used in the context of Proof Carrying Code. The primary focus shall be on type-based mechanisms for enforcing type safety and information flow policies, but I shall also discuss using logical methods to verify program correctness, and describe algorithms that transform proofs of source prgorams into proofs of executable code.

Automatic Analysis of Hybrid Systems
Embedded digital systems have become ubiquitous in everyday life. Many such systems, including many of the safety-critical ones, operate within or comprise tightly coupled networks of both discrete-state and continuous-state components. The behavior of such hybrid discrete-continuous systems cannot be fully understood without explicitly modeling and analyzing the tight interaction of their discrete switching behavior and their continuous dynamics, as mutual feedback confines fully separate analysis to limited cases. Tools for building such integrated models and for simulating their approximate dynamics are commercially available, e.g. Simulink with the Stateflow extension. Simulation is, however, inherently incomplete and has to be complemented by verification, which amounts to showing that the coupled dynamics of the embedded system and its environment is well-behaved, regardless of the actual disturbance and the influences of the application context, as entering through the open inputs of the system under investigation. Basic notions of being well-behaved demand that the system under investigation may never reach an undesirable state (safety), that it will converge to a certain set of states (stabilization), or that it can be guaranteed to eventually reach a desirable state (progress).

Within this school, we concentrate on automatic verification and analysis of hybrid systems, with a focus on fully symbolic methods manipulating both the discrete and the continuous state components symbolically by means of predicates. We provide an introduction to hybrid discrete-continuous systems, demonstrate the use of predicative encodings for compactly encoding operational high-level models, and continue to a number of methods for automatically analyzing safety, stability, and progress.

Model Checking of Action-Based Concurrent Systems
Asynchronous systems are present in a variety of domains, such as telecommunication protocols, embedded software, or multiprocessor architectures. These systems typically consist of a set of computing entities (processes or agents) executing in parallel and communicating by message-passing. Their behaviour is therefore complex and must be analyzed formally in order to detect and correct design errors as early as possible. Several formalisms have been defined for specifying the behaviour of asynchronous systems, among which networks of communicating automata, process algebras, and mu-calculi. The semantic models underlying these formalisms are the so-called labeled transition systems (LTSs), which are state/transition graphs describing the behaviour of asynchronous systems in terms of the actions.

We give an overview of these formalisms and show how they can be used to specify the behaviour of various asynchronous systems. We also present the main verification methods operating on LTSs, namely equivalence checking and model checking, and we illustrate their practical implementation and usage by means of CADP, a state-of-the-art verification toolbox for asynchronous systems.

Software Model Checking
Ensuring correctness of software systems is an increasingly challenging task due to the rapidly growing size and complexity of software. Moreover, software systems play an increasing role in safety-critical embedded systems, where dedicated hardware parts are gradually being replaced with generic architectures with dedicated software running on top of them. There is therefore an increasing need for automatic tools to formally verify software systems. However, such systems have in general very large or even infinite state spaces, and hence they are not directly amenable to classical finite-state verification methods.

Approximate verification techniques can be used to verify large systems that are beyond the reach of classical model checking. These techniques are based on property-preserving abstractions of the semantics of the system. Abstractions were first designed manually, but automatic techniques such as predicate abstraction and CEGAR (counter-example guided abstraction refinement) have recently led to fully automatic and successful tools for the verification of large software systems.

In these lectures, I will present the two main theoretical frameworks for software verification by abstraction: abstract interpretation and abstract model refinement. Algorithms to automatically construct abstract models from program sources will be presented, as well as an overview of several refinement methods. Several variants of the CEGAR approach will be compared. I will also discuss symbolic verification of some classes of infinite-state abstract models that arise from software constructs such as recursion or thread creation.

General Organization

• Stephan Merz
• Christoph Weidenbach

Local Organization

• Manuel Lamotte
• Roxane Wetzel

For comments or questions send an email to Roxane Wetzel (wetzel (at) mpi-inf.mpg.de).