Advanced Analysis Techniques is a short course held at the Danish Technical University 2012, with emphasis on SMT and the Z3 SMT solver.
The PhD-course 02913 on “Advanced Analysis Techniques” takes place in building 322 room 105 at DTU starting Monday, January 2nd at 9.00 and will be organized by Hanne Riis Nielson and Flemming Nielson and will feature Nikolaj Bjørner as invited teacher.
To sign up for the course you should register at CampusNet or contact the organizers.
For formalities please take a look at http://www.kurser.dtu.dk/02913.aspx?menulanguage=en-GB
SAT and SMT solving have advanced rapidly over the last decade and are able to deal with problems of quite impressive size. This course will give an introduction to SAT and SMT solving and hands-on experience with the Z3 SMT solver being developed by Microsoft Research.
In a Personal Project you are supposed to apply the methods and techniques to a problem related to your research or to consider one of the projects suggested during the course.
The main part of the teaching will take part during the period January 2nd – January 13th; the main part of the project work will take place during the period January 16th – January 27th (but projects can be finished earlier: at the end of the three week period on January 20th). Here is a set of project proposals.
January 2nd: Welcome. An Introduction to SAT Solving.
- Reading ,  (SAT part)
- Lab: Take a look at [b], [d].
- Slides: SAT Solving
A refresher on Propositional and First-Order Logic By Aditya Nori
An introduction to modern SAT solving
January 3rd: An Introduction to SMT Solving.
- Reading , .
- Lab: SAT and Bit-vector problems (I)
- Slides: SMT Solving
An introduction to SMT solving
January 4th: An introduction to the SMT solver Z3 and applications.
- Reading , [g].
- Lab: SAT and Bit-vector problems (II)
- Slides: Selected Applications of Z3, An introduction to Z3
January 5th: Integrating Decision Procedures (Functions and Arrays)
- Reading  (again, SMT part), ,  (first 5 sections).
- Lab: Modeling with functions and arrays. (chapter 4 of exercises)
- Slides: Decision procedures for functions and arrays
January 6th: Integrating Decision Procedures (Arithmetic)
- Reading [A] or [B], 
- Lab: Modeling with arithmetic.
- Slides: Decision procedures: Arithmetic, Data-types and other theories
January 9th: Self study.
January 10th: Problem solving with SMT procedures.
- Reading , [g]
- Lab: Solve and optimize.
- Slides: Engineering Theories with Z3
- Sample code: Partial Orders, Optimization, HOL
January 11th: Quantifiers, Theories and Decision Procedures
- Reading 
- Lab: Modeling with quantifiers.
- Slides: Matching-based quantifier instantiation,
Model-based Quantifier Instantiation,
- Project work in a topic we discuss during the first week. The topic will be adjusted according to your interests. To give an idea, possible topic areas include:
- Introductory modeling and solving using Z3-based tools (available from http://rise4fun.com)
- Develop a custom scheduling solver on top of Z3. See eg.,  and http://lara.epfl.ch/~psuter/articles/KoksalETAL12ConstraintsAsControl.pdf
- Develop a symbolic execution engine for static program analysis.
- Encode bounded model checking problems for your favorite specification language with Z3.
- Outlines of addtional project topics are here.
January 20th or January 27th: Personal Projects to be handed in (as you choose).
 Boolean Satisfiability: From Theoretical Hardness to Practical Success. Sharad Malik, Lintao Zhang. Communications of the ACM, vol.52 no.8, 2009.
 Satisfiability Modulo Theories: Introduction and Applications. Leonardo De Moura, Nikolaj Bjørner. Communications of the ACM, vol.54 no.9, 2011.
 Z3 – an Efficient SMT solver. Leonardo De Moura, Nikolaj Bjørner
 Abstract DPLL and Abstract DPLL Modulo Theories. Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli
 Generalized, Efficient Decision Procedures for Arrays. Leonardo De Moura, Nikolaj Bjørner
 Engineering Theories with Z3. Nikolaj Bjørner
 Applications of SMT solvers. Draft chapter, 2012. Leonardo De Moura, Nikolaj Bjørner
 Efficient E-matching for SMT solvers. Leonardo de Moura and Nikolaj Bjørner. CADE 2007. PDF.
 Tractability and Modern Satisfiability Modulo Theories Solvers. Leonardo de Moura and Nikolaj Bjørner. Draft chapter for Advances in Tractability, 2012.
 A Fast Linear-Arithmetic Solver for DPLL(T), Bruno Dutertre, Leonardo de Moura. Slides
[A] Aaron R. Bradley, Zohar Manna: The calculus of computation - decision procedures with applications to verification. Springer 2007: I-XV, 1-366
[d] http://rise4fun.com/Z3/tutorial/guide (online tutorial)
[e] http://research.microsoft.com/en-us/um/redmond/projects/z3/applications.html (research papers/projects with applications of Z3)
[f] http://research.microsoft.com/en-us/events/z3sig/default.aspx (recent meeting with European Z3 users, some slides describe applications)