Relational Solver for Java Generics Type System (Dmitry Boulytchev)

We present a solver for Java generics type system implemented using relational verifier-to-solver approach. The solver finds solutions for a system of subtyping inequations with free variables and thus can be used to determine a concrete type satisfying a set of constraints. The context of this work is symbolic execution for testing and verification of Java programs.