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