Institute of Computer Languages
Compilers and Languages Group
|Datum:||Freitag, 5. August 2011|
|Ort:||TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte)|
Object ownership is useful for many applications, including program verification, thread synchronization, and memory management. However, the annotation overhead of ownership type systems hampers their widespread application. This talk addresses this issue by presenting a tunable static type inference for Generic Universe Types. In contrast to classical type systems, ownership types have no single most general typing. Our inference chooses among the legal typings via heuristics. Our inference is tunable: users can indicate a preference for certain typings by adjusting the heuristics or by supplying partial annotations for the program. We present how the constraints of Generic Universe Types can be encoded as a boolean satisfiability (SAT) problem and how a weighted Max-SAT solver finds a correct Universe typing that optimizes the weights. We implemented the static inference tool, applied our inference tool to four real-world applications, and inferred interesting ownership structures.
Werner M. Dietl is a post-doctoral research associate at the
department of Computer Science & Engineering of the University of
Washington, where he works with Prof. Michael Ernst. He is a member of
the SE.CS and WASP research groups and aims to help software engineers
produce high-quality software by enabling them to better understand
and structure their software. Previously, he was a research and
teaching assistant at the Chair of Programming Methodology, ETH
Zurich, working on his doctoral thesis under the supervision of
Prof. Peter Müller.
Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.