May 7-10, 2017 Asilomar, California
A symbolic compiler translates a program to equivalent symbolic constraints, automatically reducing model checking and synthesis to constraint solving. We show that new applications of constraint solvers require domain-specific encodings of programs to constraints. These encodings yield orders of magnitude improvements in solver efficiency but these encodings cannot be easily implemented with todays symbolic compilation.
We introduce symbolic abstractions that encapsulate the domain-specific encodings. To the client code, symbolic abstractions behave as their non-symbolic counterparts, but when their implementation is symbolically compiled, they produce the domain-specific constraints. We demonstrate the idea on the first fully symbolic checker of type systems, which can find counterexamples as large as human experts; and on a program partitioner and a parallelizer of tree computations, both of which improve classical symbolic compilers by orders of magnitude.