The usage of constraint solvers in programming languages and compilers

Question

Any more or less practical programming language and compiler have to deal with constraints. The most common constraint is types. Usually type derivation and unification is done by a straightforward algorithm (Hindley-Milner, for instance), where finally all terms in a program are assigned the unique type. If it doesn't happen, then there is an error indication.

There could be more sophisticated constraints in compilers, where the complete unification is impossible and the solution exists only under certain restrictions. Possible examples are

• Dataflow analysis. The solution of affine equality constraints can be used for loop vectorization.

• Memory management. If we have some constraints on references and data access patterns, the compiler can benefit from optimizing reference counting and garbage collection.

From the other point, constraint solvers, like Z3 or Yices, are very powerful in finding satisfiable models for different kind of constraints.

I am looking for success stories of how compilers benefit from the power of SMT solvers and what kind of tasks they are solving. I listed some areas, but I didn't find any specific examples. Can you suggest any?

Answer 1

SMT solvers are often used to implement programming languages that require extensive static verification. For example languages that employ dependent types, refinement types or statically enforced contracts often use SMT solvers.

For example Liquid Haskell as well as Microsoft's Dafny and Chalice all use Z3. Other languages, like ATS or Whiley, implemented their own solver.