Static Model Analysis with Lattice-based Ontologies
This thesis demonstrates a correct, scalable and automated method to infer
semantic concepts using lattice-based ontologies, given relatively few manual
annotations. Semantic concepts and their relationships are formalized as a
lattice, and relationships within and between program elements are expressed as
a set of constraints. Our inference engine automatically infers concepts
wherever they are not explicitly specified. Our approach is general, in that
our framework is agnostic to the semantic meaning of the ontologies that it
Where practical use-cases and principled theory exist, we provide for the
expression of infinite ontologies and ontology compositions. We also show
how these features can be used to express of value-parametrized concepts and
structured data types. In order to help find the source of errors, we also
present a novel approach to debugging by showing simplified errors paths.
These are minimal subsets of the constraints that fail to type-check, and are
much more useful than previous approaches in finding the cause of program bugs.
We also present examples of how this analysis tool can be used to express
analyses of abstract interpretation; physical dimensions and units; constant
propagation; and checks of the monotonicity of expressions.