Papers

• Erika Ábrahám, Gereon Lukas Kremer. SMT Solving for Arithmetic Theories: Theory and Tool Support, 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2017), pages 1-8, IEEE, 2017.
• Erika Ábrahám. Symbolic Computation Techniques in Satisfiability Checking, 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pages 3-10, IEEE, 2016.

Tutorials

• SAT solving in a nutshell
• SMT solving in a nutshell

Satisfiability Checking Lecture

• OVERVIEW
  
  PART I: SAT solving and eager SMT solving
  
• Propositional logic
  Examples
• SAT Solving
  Example 1
  Example 2
• First-order logic
  Historical notes on decidability results
• Eager SMT solving for equalities and uninterpreted functions
• SUMMARY 1
  
  PART II: Lazy SMT solving
  
• Lazy SMT solving
• Lazy SMT solving for equalities and uninterpreted functions
• Lazy SMT solving for linear real arithmetic
  Fourier-Motzkin variable elimination
  Simplex, Simplex in SMT
• Lazy SMT solving for integer arithmetic
  Branch-and-bound
  Gomory cuts
  The Omega test, Omega test example
• SUMMARY 2
• Lazy SMT solving for (nonlinear) real arithmetic
  Interval constraint propagation
  Subtropical satisfiability
  Virtual substitution
  Cylindrical algebraic decomposition
  Groebner bases
• SUMMARY 3