Advanced Analysis Techniques

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

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 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.

January 3rd: An Introduction to SMT Solving.

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

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

January 6th: Integrating Decision Procedures (Arithmetic)

January 9th: Self study.

January 10th: Problem solving with SMT procedures.

January 11th: Quantifiers, Theories and Decision Procedures

January 12th-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:

January 20th or January 27th: 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