Kukicha -- Efficient Yet Powerful Refinement Types for Object-Oriented Languages

Refinement type systems allow programmers to use logical conditions to constrain variable values. However, most practical refinement type systems limit their expressiveness to remain automatically decidable. Deductive verification, on the other hand, can prove more complex properties but requires more time and expertise. To combine the advantages of both approaches, we introduce Kukicha, a refinement type framework for object-oriented languages based on the cooperation of type checkers and deductive verification tools. Kukicha first performs an efficient syntactic well-typedness check. If this does not succeed, it uses a deductive verifier to prove exactly those specifications that could not be shown by the type checker, while being able to assume the rest. Unlike previous similar approaches, Kukicha supports mutable objects with strong updates, since it combines the refinement type system with uniqueness types to track aliasing and packing types to track temporary violations. We prove Kukicha’s soundness for an abstract object-oriented language and implement it for Java based on the Checker Framework, and the deductive verification tools KeY and Verifast. We evaluate our implementation by verifying the correctness of an example program and showing that Kukicha reduced the verification overhead needed for verification with KeY and Verifast.