Static Model Analysis with Lattice-based Ontologies

This thesis demonstrates a correct, scalable and automated method to infersemantic concepts using lattice-based ontologies, given relatively few manualannotations. Semantic concepts and their relationships are formalized as alattice, and relationships within and between program elements are expressed asa set of constraints. Our inference engine automatically infers conceptswherever they are not explicitly specified. Our approach is general, in thatour framework is agnostic to the semantic meaning of the ontologies that ituses.Where practical use-cases and principled theory exist, we provide for theexpression of infinite ontologies and ontology compositions. We also showhow these features can be used to express of value-parametrized concepts andstructured data types. In order to help find the source of errors, we alsopresent a novel approach to debugging by showing simplified errors paths.These are minimal subsets of the constraints that fail to type-check, and aremuch 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 expressanalyses of abstract interpretation; physical dimensions and units; constantpropagation; and checks of the monotonicity of expressions