This is a part of GSOC in Scala:

• http://www.scala-lang.org/gsoc2013

The goal of this project is to develop a reasonably efficient constraint solver in Scala. You will build on a SAT solver we are currently releasing and will add incremental SAT solving capabilities as well as reasoning about functional data structures. The constraint solver can be used for constraint programming, automated testing, verification, and synthesis in Scala.

• Regis Blanc
• Philippe Suter
• Viktor Kuncak

• LARA Software
• http://www.verit-solver.org/

• Chaff: engineering an efficient SAT solver
• Efficient conflict driven learning in a boolean satisfiability solver
• An Extensible SAT-solver (original MiniSat implementation description)

• DPLL(T): Fast Decision Procedures
• Theorem Proving using Lazy Proof Explication and the corresponding Slides on Lazy Proof Explication
• Integrating Simplex with DPLL(T) and Longer Report on Integrating Simplex with DPLL(T)
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL

• KodKod paper
• Paradox paper
• Bounded Model Generation for Isabelle/HOL
• Calculi for Program Incorrectness and Arithmetic, Philipp Rümmer's PhD thesis