More Powerful Constant Value Checking with SMT Solving

Pluggable type systems extend the basic type system of a programming language by introducing additional type hierarchies to specify more complex properties and dependencies
between variables. For Java, the Checker Framework provides various pluggable type systems
corresponding with so-called Checkers that verify the correct use of their types. One such
Checker is the Constant Value Checker, with which a user can specify restrictions on the
values a primitive integer or boolean variable can hold using a set or range of constant
values. However, the current implementation of the Value Checker makes use of a limited set
of manual typing rules that, in practice, often fail to verify well-typedness of more complex
code. The aim of this thesis is to address this limitation using SMT (Satisfiability Modulo
Theories) solvers by creating corresponding first-order logic formulas for expressions whose
type checks fail with the current implementation and determining their well-typedness
based on the satisfiability of these formulas. Furthermore, we introduce new dependent
types for specifying allowed values with expressions that can depend on other variables
... mehr
in the program. We formally prove the correctness of this extension on the basis of a
simple theoretical programming language and assess whether such an SMT value checking
subsystem is able to reduce the amount of false negative type checking results without
introducing excessive overhead using a set of sample programs.