Werner Dietl at the University of Waterloo

Werner Dietl

wdietl@uwaterloo.ca, Room EIT 4007

Electrical and Computer Engineering, University of Waterloo

Contact details & calendar

Also see my publications by date.

Applications

Building and Using Pluggable Type-Checkers (Software Engineering in Practice Track, International Conference on Software Engineering (ICSE), 2011): We built a series of pluggable type checkers using the Checker Framework, and evaluated them on 2 million lines of code, finding hundreds of bugs in the process.
EnerJ: Approximate Data Types for Safe and General Low-Power Computation — Full Proofs (TR, 2011): EnerJ is an extension to Java that adds approximate data types to allow programmers to expose hardware faults in a safe, principled manner in order to reduce energy consumption.
EnerJ: Approximate Data Types for Safe and General Low-Power Computation (Programming Language Design and Implementation (PLDI), 2011): EnerJ is an extension to Java that adds approximate data types to allow programmers to expose hardware faults in a safe, principled manner in order to reduce energy consumption.
A type system for regular expressions (Formal Techniques for Java-like Programs (FTfJP), 2012): Practical experience designing and using a type system for regular expressions.
Verification Games: Making Verification Fun (Formal Techniques for Java-like Programs (FTfJP), 2012): An overview of the Verification Games project and Pipe Jam prototype game.
ReIm & ReImInfer: Checking and inference of reference immutability and method purity (Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2012): ReIm, a type system for reference immutability, and ReImInfer, a corresponding type inference analysis.
Type Annotations, the Checker Framework, and JML (The Java Modeling Language., 2013)
JavaUI: Effects for Controlling UI Object Access (European Conference on Object-Oriented Programming (ECOOP), 2013): JavaUI is a type and effect system that prevents non-UI threads from accessing UI objects or invoking UI-thread-only methods.
Annotations on Java types (2014): This is the Proposed Final Draft of the specification of type annotations in Java 8.
Collaborative verification of information flow for a high-assurance app store (Computer and Communications Security (CCS), 2014): An information-flow type system is effective at preventing malicious apps from an app store.
Lessons Learned in Game Development for Crowdsourced Software Formal Verification (USENIX Summit on Gaming, Games, and Gamification in Security Education (3GSE), 2015): Crowd-sourcing provides the promise of making formal verification cheaper and thus more prevalent. This paper overviews 5 games by which unskilled people can perform program verification tasks.
Static analysis of implicit control flow: Resolving Java reflection and Android intents (Automated Software Engineering (ASE), 2015): Standard program analysis understand control flow through direct procedure calls. This paper provides analyses that resolve uses of Java reflecton and the data passed in Android intents.
Granullar: Gradual Nullable Types for Java (Compiler Construction (CC), 2017): Granullar is a gradual type system for null-safety.
Don't Miss the End: Preventing Unsafe End-of-File Comparisons (NASA Formal Methods, 2018): A type system that prevents unsafe EOF value comparisons statically.
Precise Inference of Expressive Units of Measurement Types (Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2020)

Scalability and Precision by Combining Expressive Type Systems and Deductive Verification (Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2021)
Least-Privilege Calls to Amazon Web Services (IEEE Transactions on Dependable and Secure Computing, 2022)
Scalable and Precise Refinement Types for Imperative Languages (International Conference on Integrated Formal Methods (iFM) PhD symposium, 2023)
OppropBERL: A GNN and BERT-style Reinforcement Learning-based Type Inference System (IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER) short papers, 2024)

Object Ownership

A Type System for Checking Applet Isolation in Java Card (Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS), 2004): A refined type system for Java Card that enables static checking of applet isolation.
Exceptions in Ownership Type Systems (Formal Techniques for Java-like Programs (FTfJP), 2004): Possible exception handling in different ownership type systems.
Universes: Lightweight Ownership for JML (Journal of Object Technology (JOT), Special Issue: ECOOP 2004 Workshop FTfJP, 2005): Introduction to object ownership and the Universe type system.
Four papers (Annual Report, 2006): Two articles and two summaries in the annual report.
Formalization of Generic Universe Types (TR, 2006): Generic Universe Types are an ownership type system for a Java-like programming language with generic types that enforces the owner-as-modifier discipline.
Four papers (Annual Report, 2007): Three summaries and one reprint in the annual report.
Generic Universe Types (Foundations and Developments of Object-Oriented Languages (FOOL/WOOD), 2007): Generic Universe Types are an ownership type system for a Java-like programming language with generic types that enforces the owner-as-modifier discipline.
Generic Universe Types (European Conference on Object-Oriented Programming (ECOOP), 2007): Generic Universe Types are an ownership type system for a Java-like programming language with generic types that enforces the owner-as-modifier discipline.
2007 State of the Universe Address (International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), 2007): This position paper summarizes recent developments related to the Universe type system and suggests directions for future work.
Runtime Universe Type Inference (International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), 2007): Inference of Universe types using traces of program executions.
Three papers (Annual Report, 2008): Reprints of three articles in the annual report.
Ownership Type Systems and Dependent Classes (Foundations of Object-Oriented Languages (FOOL), 2008): The topology of different ownership type systems can be expressed on top of dependent classes, a generalization of virtual classes.
JML Reference Manual (2008): Work on the Universe type system chapter.
Universe Type System — Quick-Reference (2008): Quick reference for the Universe type system, providing an overview and summarizing the type rules and the usage of the tools.
Universe Types for Topology and Encapsulation (Formal Methods for Components and Objects (FMCO), 2008): Extensive type-theoretic account of the Universe Type System, with explanations and complete proofs, and the clean separation of the topological from the encapsulation concerns.
Comparing Universes and Existential Ownership Types (International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), 2009): Formalizes a parametric ownership system with existential quantification of contexts and gives a formal translation between programs written in this language and using Universe types.
Comparing Universes and Existential Ownership Types (TR, 2009): Formalizes a parametric ownership system with existential quantification of contexts and gives a formal translation between programs written in this language and using Universe types.
Tunable Universe Type Inference (TR, 2009): A tunable type inference for Universe types.
Universe Types: Topology, Encapsulation, Genericity, and Tools (Ph.D. dissertation, 2009): Generic Universe Types are a sound, lightweight ownership type system for type-generic object-oriented programming languages, which cleanly separates the ownership topology from the owner-as-modifier encapsulation discipline and is supported by a comprehensive set of tools. Thesis nominated by ETH Zurich for the 2009 GI Outstanding Dissertation Award.
Universe Types: Topology, Encapsulation, Genericity, and Tools (2010): Available in German only. See [DietlPhD09].
Separating ownership topology and encapsulation with Generic Universe Types (ACM Transactions on Programming Languages and Systems, 2011): Generic Universe Types structure the heap hierarchically and separate the enforcement of an ownership topology from an encapsulation system.
Tunable Static Inference for Generic Universe Types (European Conference on Object-Oriented Programming (ECOOP), 2011): A tunable static type inference for Generic Universe Types.
Inference and Checking of Object Ownership (European Conference on Object-Oriented Programming (ECOOP), 2012): A static type inference for Universe Types and Ownership Types.
Object Ownership in Program Verification (Aliasing in Object-Oriented Programming, 2013): We present two ownership systems that have been designed specifically to support program verification — Universe Types and Spec#'s Dynamic Ownership — and explain their applications in program verification, illustrated through a series of Spec# examples.
A Computational Complexity Analysis of Tunable Type Inference for Generic Universe Types (Theoretical Computer Science, 2020)

Image Watermarking

Watermark Security via High-Resolution Wavelet Filter Parametrization (International Scientific Conference, Section 1: Applied Mathematics, 2002)
Improving the Security of Wavelet-based Watermarking Systems (Masters thesis, 2002): This thesis presents two methods to improve the security of wavelet-based watermarking systems and analyzes their properties in detail. It won the Excellent Diploma Thesis Award from the Austrian Computer Society (OCG, http://www.ocg.at/).
Key-dependent Pyramidal Wavelet Domains for Secure Watermark Embedding (Electronic Imaging, Security and Watermarking of Multimedia Contents V, 2003): Using wavelet filter parametrization to add security to wavelet based watermarking schemes.
Protection of Wavelet-based Watermarking Systems using Filter Parametrization (Signal Processing (Special Issue on Security of Data Hiding Technologies), 2003): Using wavelet filter parametrization as a means to add security to wavelet-based watermarking schemes.
Watermark Security via Secret Wavelet Packet Subband Structures (Communications and Multimedia Security, 2003): Using the vast amount of possible wavelet packet decomposition structures to create a secret wavelet domain that improves the security of watermarking schemes.
Robustness against Unauthorized Watermark Removal Attacks via Key-dependent Wavelet Packet Subband Structures (International Conference on Multimedia and Expo (ICME), 2004): Using random wavelet packet decompositions to increase the security of watermarking systems against unauthorized removal attacks.
Key-Dependency for a Wavelet-Based Blind Watermarking Algorithm (Multimedia and Security Workshop, 2004): Embedding multiple watermarks in the wavelet domain.

Publications by Topic

Applications

Object Ownership

Image Watermarking