May 7-10, 2017 Asilomar, California
A symbolic compiler translates a program to symbolic constraints, automatically reducing model
checking and synthesis to constraint solving. We show that new applications of constraint solving
require domain-specific encodings that yield the required orders of magnitude improvements
in solver efficiency. Unfortunately, these encodings cannot be obtained with today’s symbolic
We introduce symbolic languages that encapsulate domain-specific encodings under abstractions that behave as their non-symbolic counterparts: client code using the abstractions can be tested and debugged on concrete inputs. When client code is symbolically compiled, the resulting constraints use domain-specific encodings.
We demonstrate the idea on the first fully symbolic checker of type systems; a program partitioner; and a parallelizer of tree computations. In each of these case studies, symbolic languages improved on classical symbolic compilers by orders of magnitude.