Tutorial 1:	Testing, Optimization, and Games (by Mihalis Yannakakis) Yannakakis_ATVA2006_Tutorial.pdf
	We will discuss algorithmic problems arising in the testing of reactive systems (i.e. systems that interact with their environment), modeled by various types of state machines. The goal is to design test sequences so that we can deduce desired information about the given system under test, such as whether it conforms to a given specification model, or whether it satisfies given requirement properties. Test generation can be approached from different points of view - as an optimization problem of minimizing cost and maximizing the effectiveness of the tests; as a game between tester and system under test; or as a learning problem. We touch on some of these aspects and related algorithmic questions.
Tutorial 2:	Introduction to Generalized Symbolic Trajectory Evaluation (by Jin Yang) Yang_ATVA2006_Tutorial.pdf
	Generalized Symbolic Trajectory Evaluation (GSTE) is a symbolic model checking approach that combines the high capacity of STE with the expressive power of traditional symbolic model checking. It has been successfully applied to the formal verification of complex Intel micro-processor designs with tens of thousands of state elements. GSTE uses an operational style specification for describing a functional property of a hardware circuit. Model checking in GSTE is based on a form of symbolic simulation with a tightly integrated dynamic quaternary abstraction mechanism that explores the shape of the specification to achieve high verification capacity. As such, the complexity of model checking in GSTE mostly depends on the complexity of the specification rather than the complexity of the circuit under verification. A brief introduction to some of the key aspects of GSTE is to be given.
Tutorial 3:	Secrets of SLAM (by Thomas Ball) Ball_ATVA2006_Tutorial.pdf
	Model checking is a technique to find bugs in systems by systematically exploring their state spaces. Due to state space explosion, model checkers typically operate on a manually constructed finite-state abstraction of the system. The goal of the SLAM project is to model check software written in common programming languages directly. SLAM has been successfully used to find and fix errors in Windows device drivers written in the C language. SLAM operates by automatically constructing and refining model-checkable abstractions (called Boolean Programs) of a C program. The first part of this tutorial will describe how the SLAM project has combined and extended results from the areas of program analysis, model checking and theorem proving to analyze critical properties of systems software written in the C language. The second half of the tutorial will present some of the engineering "secrets" we applied to the basic SLAM process to improve its performance on Windows device drivers.