Student Project: Static Universe Type Inference using a SAT-Solver
Download: PDF.
“Static Universe Type Inference using a SAT-Solver” by Matthias Niklaus. June 2006. Master's thesis.
Abstract
The Universe type system allows to restrict the possible aliasing in object-oriented programs and thereby enables static reasoning about individual components. Compared to other ownership type systems, the Universe type system is lightweight, but annotating existing software is still a considerable effort. To ease the effort of annotation, static inference of Universe modifiers from Java source code is an interesting problem. In this work, we investigated the use of pseudo-boolean optimizers to find Universe annotations. To show the benefit of the new backend we implemented a new static Universe type inferer. The results reveal that also heavy annotated programs can be typed correctly. This report presents the architecture, implementation, and results of the new tool.
Download: PDF.
BibTeX entry:
@unpublished{MNiklaus06,
author = {Matthias Niklaus},
title = {{Static Universe Type Inference using a SAT-Solver}},
month = jun,
note = {Master's thesis}
}
Back to the student projects sorted by date or by category.
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author’s copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
(This webpage was created with bibtex2web.)