The PhD-course 02913 on “Advanced Analysis Techniques” takes place in building 322 room 105 at DTU starting Monday, January 2^nd 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

Motivation:

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.

Teaching Schedule:

The main part of the teaching will take part during the period January 2^nd – January 13^th; the main part of the project work will take place during the period January 16^th – January 27^th (but projects can be finished earlier: at the end of the three week period on January 20^th). Here is a set of project proposals.

January 2^nd: Welcome. An Introduction to SAT Solving.

• Reading [1], [4] (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 3^rd: An Introduction to SMT Solving.

• Reading [2], [7].
• Lab: SAT and Bit-vector problems (I)
• Slides:  SMT Solving
             An introduction to SMT solving

January 4^th: An introduction to the SMT solver Z3 and applications.

• Reading [3], [g].
• Lab: SAT and Bit-vector problems (II)
• Slides: Selected Applications of Z3, An introduction to Z3

January 5^th: Integrating Decision Procedures (Functions and Arrays)

• Reading [4] (again, SMT part), [5], [9] (first 5 sections).
• Lab: Modeling with functions and arrays. (chapter 4 of exercises)
• Slides: Decision procedures for functions and arrays

January 6^th: Integrating Decision Procedures (Arithmetic)

• Reading [A] or [B], [10]
• Lab: Modeling with arithmetic.
• Slides: Decision procedures: Arithmetic, Data-types and other theories

January 9^th: Self study.

January 10^th: Problem solving with SMT procedures.

• Reading [6], [g]
• Lab: Solve and optimize.
• Slides: Engineering Theories with Z3
• Sample code: Partial Orders, Optimization, HOL

January 11^th: Quantifiers, Theories and Decision Procedures

• Reading [8]
• Lab: Modeling with quantifiers.
• Slides: Matching-based quantifier instantiation, 
            Saturation-based procedures,
            Model-based Quantifier Instantiation,
            Quantifier Elimination

January 12^th-onwards:

• 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., [6] 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 20^th or January 27^th: Personal Projects to be handed in (as you choose).

Selected Papers:

[1] Boolean Satisfiability: From Theoretical Hardness to Practical Success. Sharad Malik, Lintao Zhang. Communications of the ACM, vol.52 no.8, 2009.

[2] Satisfiability Modulo Theories: Introduction and Applications. Leonardo De Moura, Nikolaj Bjørner. Communications of the ACM, vol.54 no.9, 2011.

[3] Z3 – an Efficient SMT solver. Leonardo De Moura, Nikolaj Bjørner

[4] Abstract DPLL and Abstract DPLL Modulo Theories. Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli

[5] Generalized, Efficient Decision Procedures for Arrays. Leonardo De Moura, Nikolaj Bjørner

[6] Engineering Theories with Z3. Nikolaj Bjørner

[7] Applications of SMT solvers. Draft chapter, 2012. Leonardo De Moura, Nikolaj Bjørner

[8] Efficient E-matching for SMT solvers. Leonardo de Moura and Nikolaj Bjørner. CADE 2007. PDF.

[9] Tractability and Modern Satisfiability Modulo Theories Solvers. Leonardo de Moura and Nikolaj Bjørner. Draft chapter for Advances in Tractability, 2012.

[10] A Fast Linear-Arithmetic Solver for DPLL(T), Bruno Dutertre, Leonardo de Moura. Slides

Textbooks:

[A] Aaron R. Bradley, Zohar Manna: The calculus of computation - decision procedures with applications to verification. Springer 2007: I-XV, 1-366

[B] Daniel Kroening and Ofer Strichman: Decision Procedures, an algorithmic point of view. http://www.decision-procedures.org/

Web resources:

[a] http://research.microsoft.com/projects/z3

[b] http://rise4fun.com/z3

[c] http://smtlib.org

[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)

[g] Tutorial guide with samples on using Z3's API