Type-based Object Immutability with Flexible Initialization (2009)
Abstract. We present a type system for checking object immutability, reference immutability, and class immutability in an open or closed world. In order to separate object initialization from object...
Explicit information flow properties in JML (2009)
Christian Haack, Erik Poll, Aleksy Schubert
Abstract This paper considers how explicit information flow properties can be expressed and verified in a traditional program logic, using pre- and postconditions. As concrete specification language...
Named in memory of Alonzo Church. (2008)
Joe Wells, Christian Haack, Boston Coll, Bob Muller, Geoff Washburn, Ian Westmacott, ...
squashing typing derivations in systems with intersection types
Separation Logic Contracts for a Java-like Language with Fork/Join (2008)
Haack, Christian, Hurlin, Clément
We adapt a variant of permission-accounting separation logic to a concurrent Java-like language with fork/join. To support both concurrent reads and information hiding, we combine fractional...
Separation Logic Contracts for a Java-like Language with Fork/Join (2008)
Haack, Christian, Hurlin, Clément
We adapt a variant of permission-accounting separation logic to a concurrent Java-like language with fork/join. To support both concurrent reads and information hiding, we combine fractional...
Separation Logic Contracts for a Java-like Language with Fork/Join (2008)
Haack, Christian, Hurlin, Clément
We adapt a variant of permission-accounting separation logic to a concurrent Java-like language with fork/join. To support both concurrent reads and information hiding, we combine fractional...
Separation Logic Contracts for a Java-like Language with Fork/Join (2008)
Haack, Christian, Hurlin, Clément
We adapt a variant of permission-accounting separation logic to a concurrent Java-like language with fork/join. To support both concurrent reads and information hiding, we combine fractional...
Separation logic contracts for a Java-like language with fork/join (2008)
Haack, Christian, Hurlin, Clément
We adapt a variant of permission-accounting separation logic to a concurrent Java-like language with fork/join. To support both concurrent reads and information hiding, we combine fractional...
Reasoning about Java's reentrant locks (2008)
Haack, Christian, Huisman, Marieke, Hurlin, Clément
This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permission-accounting separation logic. As usual, each...
Separation logic contracts for a Java-like language with fork/join (2008)
Haack, Christian, Hurlin, Clément
We adapt a variant of permission-accounting separation logic to a concurrent Java-like language with fork/join. To support both concurrent reads and information hiding, we combine fractional...
Reasoning about Java's reentrant locks (2008)
Haack, Christian, Huisman, Marieke, Hurlin, Clément
This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permission-accounting separation logic. As usual, each...
Using the Smash Product to Compose Data Flow Analyses (2007)
Ionut Buricea Christian, Christian Haack, Corina Pasareanu
Introduction Assume a dataflow analysis consists of a lattice L and a system of transition functions F . We propose to compose two dataflow analyses (L 1 ; F 1 ) and (L 2 ; F 2 ) into an analysis (L...
Christian Haack, Alan Jeffrey, A B {|#(m
Verifying secrecy and authenticity in the Dolev–Yao model. Verification techniques applied to this. logics for authentication (BAN logic) fully automatic techniques: model-checking (e.g. Caspar,...
Timed spi-calculus with types for secrecy and authenticity (2005)
Abstract. We present a discretely timed spi-calculus. A primitive for key compromise allows us to model key compromise attacks, thus going beyond the standard Dolev–Yao attacker model. A primitive...
Pattern-Matching Spi-Calculus (2004)
Abstract. Cryptographic protocols often make use of nested cryptographic primitives, for example signed message digests, or encrypted signed messages. Gordon and Jeffrey’s prior work on types for...
Type Error Slicing in Implicitly Typed Higher-Order Languages (2004)
Previous methods have generally identified the location of a type error as a particular program point or the program subtree rooted at that point. We present a new approach that identifies the...
Type Error Slicing in Implicitly Typed Higher-Order Languages (2003)
Previous methods have generally identified the location of a type error as a particular program point or the program subtree rooted at that point. We present a new approach that identifies the...
Academic Degrees Home Address: (2003)
Christian Haack, Molenweg A, Christian Haack
Type systems for programming languages and security Software specification and verification Language-based security Verification of security protocols
Although systems with intersection types have many unique capabilities, there has never been a fully satisfactory explicitly typed system with intersection types. We introduce and prove the basic...
Although systems with intersection types have many unique capabilities, there has never been a fully satisfactory explicitly typed system with intersection types. We introduce # with branching types...
Thesis (Ph. D.)--Kansas State University, 2001.
A Decomposition Theorem for Domains (1995)
Christian Haack, Christian Haack
A domain constructor that generalizes the product is defined. It is shown that with this constructor exactly the prime-algebraic coherent Scott-domains and the empty set can be generated from...
Pattern Matching Spi-Calculus (1964)
Cryptographic protocols often make use of nested cryptographic primitives, for example signed message digests, or encrypted signed messages. Gordon and Jeffrey’s prior work on types for...