Flow-sensitive type qualifiers.
We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled flow-sensitively---the underlying standard types are unchanged, which allows us to obtain an efficient constraint-based inference algorithm that integrates flow-insensitive alias analysis, effect inference, and ideas from linear type systems to support strong updates. We demonstrate the usefulness of flow-sensitive type qualifiers by finding a number of new locking bugs in the Linux kernel.
INTRODUCTION
Standard type systems are flow-insensitive, meaning a
value's type is the same everywhere. However, many important
program properties are flow-sensitive. Checking such
properties requires associating di#erent facts with a value at
di#erent program points.
This paper shows how to extend standard type systems
with user-specified flow-sensitive type qualifiers, which are
atomic properties that refine standard types. In our system
users annotate programs with type qualifiers, and inference
checks that the annotations are correct. The critical feature
of our approach is that flow-sensitivity is restricted to the
type qualifiers that decorate types-the underlying standard
types are unchanged-which allows us to obtain an e#cient
type inference algorithm. Type qualifiers capture a natural
class of flow-sensitive properties, while e#cient inference of
the type qualifiers allows us to apply an implementation to
large code bases with few user annotations.
As an example of type qualifiers, consider the type File
used for I/O operations on files. In most systems File operations
can only be used in certain ways: a file must be
opened for reading before it is read, it must be opened for
writing before it is written to, and once closed a file cannot
be accessed. We can express these rules with flow-sensitive
type qualifiers. We introduce qualifiers open, read, write,
readwrite, and closed. The type open File describes a
file that has been opened in an unknown mode, the type
read File (respectively write File) is a file that is open
for reading (respectively writing), the type readwrite File
is a file open for both reading and writing, and the type
closed File is a closed file. These qualifiers capture inherently
flow-sensitive properties. For example, the close()
function takes an open File as an argument and changes
the file's state to closed File.
These five qualifiers have a natural subtyping relation:
readwrite # read # open and readwrite # write # open.
The qualifier closed is incomparable to other qualifiers because
a file may not be both closed and open. Qualifiers that
introduce subtyping are very common, and our framework
supports subtyping directly; in addition to a set of qualifiers,
users can define a partial order on the qualifiers.
Our results build on recent advances in flow-sensitive type
systems [5, 7, 25] as well as our own previous work on flow-insensitive
type qualifiers [16, 24]. The main contribution
of our work is a practical, flow-sensitive type inference al-
gorithm, in contrast to the type checking systems of [5, 7,
Our flow-sensitive type inference algorithm is made practical
by solving constraints lazily. As in any flow-sensitive
analysis, explicitly forming a model of the store at every program
point is prohibitively expensive for large code bases.
By generating a constraint system linear in the size of the
type-annotated program and solving only the portion of the
constraints needed to check qualifier annotations, our algorithm
is able to scale to large examples.
Finally, our system is designed to be sound; we aim to
prove the absence of bugs, not just to be heuristically good
at finding bugs. For example, we believe that our system
could be integrated into Java in a sound manner. We have
shown soundness for restrict (Section 4), a key new construct
in our system (see technical report [15]). Since the
remainder of our system can be viewed as a simplification
of [25], we believe it is straightforward to prove soundness
for our full type system using their techniques.
In Section 5 we report on experience with two applica-
tions, analyzing locking behavior in the Linux kernel and
analyzing C stream library usage in application code. Our
system found a number of new locking bugs, including some
that extend across multiple functions or even, in one case,
across multiple files.
1.1 System Architecture
Our flow-sensitive qualifier inference algorithm has several
interlocking components. We first give an overview of the
major pieces and how they fit together.
We expect programmers to interact with our type sys-
tem, both when adding qualifier annotations and when reviewing
the results of inference. Thus, we seek a system
that supports e#cient inference and is straightforward for
a programmer to understand and use. Our type inference
system integrates alias analysis, e#ect inference, and ideas
from linear type systems.
. We use a flow-insensitive alias analysis to construct a
model of the store. The alias analysis infers an abstract
location for the result of each program expression; expressions
that evaluate to the same abstract location
may be aliased.
. We use e#ect inference [20] to calculate the set of abstract
locations an expression e might use during e's
evaluation. These e#ects are used in analyzing function
calls and restrict (see below). E#ect inference
is done simultaneously with alias analysis.
. We model the state at a program point as an abstract
store, which is a mapping from abstract locations to
types. We can use the abstract locations from the flow-insensitive
alias analysis because we allow only the
type qualifiers, and not the underlying standard types,
to change during execution. We represent abstract
stores using a constraint formalism. Store constructors
model allocations, updates, and function calls,
and store constraints C1 # C2 model a branch from
the program point represented by store C1 to the program
point represented by store C2 .
. We compute a linearity [25] for each abstract location
at each program point. Informally, an abstract location
is linear if the type system can prove that it corresponds
to a single concrete location in every execution;
otherwise, it is non-linear. We perform strong updates
[4] on locations that are linear and weak updates on
locations that are non-linear. A strong update can
change the qualifier on a location's type arbitrarily.
Weak updates cannot change qualifiers. Computing
linearities is important because most interesting flow-sensitive
properties require strong updates.
. The system described so far has a serious practical
weakness: Type inference may fail because a location
on which a strong update is needed may be inferred
to be non-linear. We address this with a new annotation
restrict. The expression restrictx =e in e #
introduces a new name x bound to the value of e. The
name x is given a fresh abstract location, and among
all aliases of e, only x and values derived from x may be
used within e # . Thus the location of x may be linear,
and hence may be strongly updated, even if the location
of e is non-linear. We use e#ects to enforce the correctness
of restrict expressions-soundness requires
that the location of e does not appear in the e#ect of
e # .
. We use e#ects to increase the precision of the analysis.
If an expression e does not reference location #, which
we can determine by examining the e#ect of e, then it
does not access the value stored at #, and the analysis
of # can simply flow from the store preceding e to the
one immediately after e without passing through e. If e
is an application of a function called in many di#erent
contexts, then this idea makes e fully polymorphic in
all the locations that e does not reference.
2. RELATED WORK
We discuss three threads of related work: type systems,
dataflow analysis, and tools for finding bugs in software.
Type Systems. Our type system is inspired by region and
alias type checking systems designed for low-level programs
[5, 25, 29]. Two recent language proposals, Vault [7] and
Cyclone [17], adapt similar ideas for checking high-level pro-
grams. Both of these languages are based on type checking
and require programmers to annotate their programs with
types. In contrast, we propose a simpler and less expressive
monomorphic type system that is designed for e#cient type
Our system incorporates e#ect inference [20, 32]
to gain a measure of polymorphism. Recent work on Vault
[12] includes a construct focus that is similar to restrict.
The type state system of NIL [27] is one of the earliest
to incorporate flow-sensitive type checking. Xu et al [33]
use a flow-sensitive analysis to check type safety of machine
code. Type systems developed for Java byte code [22, 26]
also incorporate flow-sensitivity to check for initialization
before use and to allow reuse of the same local variable with
di#erent types.
Igarashi and Kobayashi [18] propose a general framework
for resource usage analysis, which associates a trace with
each object specifying valid accesses to the object and checks
that the program satisfies the trace specifications. They
provide an inference algorithm, although it is unclear how
e#cient it is in practice since it invokes as a sub-step an
unspecified algorithm to check that a trace set is valid.
Flanagan and Freund [13] use a type checking system to
verify Java locking behavior. In Java locks are acquired and
released according to a lexical discipline. To model locking
in the Linux kernel (as in Section 5) we must allow non-
lexically scoped lock acquires and releases.
The subset of our system consisting of alias analysis and
e#ect inference can be seen as a monomorphic variant of
region inference [28]. The improvements to region inference
reported in [2] are a much more expensive and precise
method for computing linearities.
Dataflow Analysis. Although our type-based approach is
related to dataflow analysis [1], it di#ers from classical dataflow
analysis in several ways. First, we generate constraints over
stores and types to model the program. Thus there is no distinction
between forward and backward analysis; information
may flow in both directions during constraint resolution,
depending on the specified qualifier partial order. Second,
we explicitly handle pointers, heap-allocated data, aliasing,
and strong/weak updates. Third, there is no distinction between
interprocedural and intraprocedural analysis in our
system.
The strong/weak update distinction was first described
by Chase et al [4]. Several techniques that allow strong updates
have been proposed for dataflow-based analysis of programs
with pointers, among them [3, 8, 31]. Jagannathan
et al [19] present a system for must-alias analysis of higher-order
languages. The linearity computation in our system
corresponds to their singleness computation, and they use
a similar technique to gain polymorphism by flowing some
bindings around function calls.
Another recent system for checking typestate properties is
ESP [6]. Like our proposal, ESP incorporates a conservative
alias analysis. There are also significant di#erences: ESP is
more directly based on dataflow analysis and incorporates a
path-sensitive symbolic execution component. ESP has been
used to check the correctness of C stream library usage in
gcc.
Bug-Finding Tools. The AST Toolkit provides a frame-work
for posing user-specified queries on abstract syntax
trees annotated with type information. The AST Toolkit
has been successfully used to uncover many bugs [30].
Meta-level compilation [9] is a system for finding bugs in
programs. The programmer specifies a flow-sensitive property
as an finite state automaton. A program is analyzed by
traversing control paths and triggering state transitions of
the automata on particular actions in program statements.
The system warns of potential errors when an automaton enters
an error state. In [9] an intraprocedural analysis of lock
usage in the Linux kernel uncovered many local locking bugs.
Our type-based system found interprocedural locking bugs
that extended across multiple functions or even, in one case,
across multiple files (Section 5). 1 Newer work on meta-level
compilation [10] includes some interprocedural dataflow, but
it is unclear how their interprocedural dataflow analysis handles
aliasing.
LCLint [11] is a dataflow-based tool for checking properties
of programs. To use LCLint, the programmer adds
extra annotations to their program. LCLint performs flow-sensitive
intraprocedural analysis, using the programmer's
1 The bugs were found in a newer version of the Linux kernel
than examined by [9], so a direct comparison is not possible,
though these bugs cannot be found by purely intraprocedural
analysis.
annotations at function calls.
ESC/Java [14] is a tool for finding errors in Java programs.
ESC/Java uses sophisticated theorem-proving technology to
verify program properties, and it includes a rich language for
program annotations.
3. TYPE SYSTEM
We describe our type system using a call-by-value lambda
calculus extended with pointers and type qualifier annota-
tions. The source language is
e ::= x | n | #x.e | e1 e2 | ref e | !e | e1 := e2
| assert(e, Q) | check(e, Q)
Here x is a variable, n is an integer, #x.e is a function with
argument x and body e, the expression e1 e2 is the application
of function e1 to argument e2 , the expression ref e
allocates memory and initializes it to e, the expression !e
dereferences pointer e, and the expression e1 := e2 assigns
the value of e2 to the location e1 points to.
We introduce qualifiers into the source language by adding
two new forms [16]. The expression assert(e, Q) asserts
that e's top-level qualifier is Q, and the expression check(e, Q)
type checks only if e's top-level qualifier is at most Q.
Our type inference algorithm is divided into two steps.
First we perform an initial flow-insensitive alias analysis and
e#ect inference. Second we generate and solve store and
qualifier constraints and compute linearities.
3.1 Alias Analysis and Effect Inference
We present the flow-insensitive alias analysis and e#ect inference
as a translation system rewriting source expressions
to expressions decorated with locations, types, and e#ects.
The target language is
| assert(e, Q) | check(e, Q)
The target language extends the source language syntax in
two ways. Every allocation site ref # e is annotated with
the abstract location # that is allocated, and each function
annotated with both the type t of its parameter
and the e#ect L of calling the function. E#ects are unions
and intersections of e#ect variables #, which represent an
unknown set of e#ects that e#ect inference solves for, and
e#ect constants #, which stands for either a read, write, or
allocation of location #. For simplicity in this paper we do
not distinguish which of the three possible e#ects # stands
for, although we do so in our implementation.
Foreshadowing flow-sensitive analysis, pointer types are
written ref (#), and we maintain a separate global abstract
store CI mapping locations # to types; CI (# if location
# contains data of type # . If type inference requires # ,
we also require CI
contain the e#ect L of calling the function.

Figure

1 gives rules for performing alias analysis and effect
inference while translating source programs into our
target language. This translation system proves judgments
meaning that in type environment #, expression
e translates to expression e # , which has type t, and
the evaluation of e may have e#ect L.
(Ref)
(Deref)
(App)
(Down)

Figure

1: Type, alias, and e#ect inference
The set of locations appearing in a type, locs(t), is
locs(ref (# locs(CI (#))
locs(t1 -# L t2
We assume that locs(#) is empty until # is equated with a
constructed type. We define locs(#) to be
locs(t).
We briefly discuss the rules in Figure 1:
. (Var) and (Int) are standard. In lambda calculus, a
variable is an r-value, not an l-value, and accessing a
variable has no e#ect.
. (Ref) allocates a fresh abstract location #. We add the
e#ect {#} of the allocation to the e#ect and record in
CI the type to which the location # points.
. (Deref) evaluates e, which yields a value of type t. As
is standard in type inference, to compute the location
e points to we create a fresh location # and equate the
type t with the type ref (#). We look up the type of
location # in CI and add # to the e#ect set.
. (Assign) writes a location. Note that the type of e2
and the type that e1 points to are equated. Because
types contain locations, this forces potentially aliased
locations to be modeled by one abstract location.
. (Lam) defines a function. We annotate the function
with the e#ect # of the function body and the type #
of the parameter. Function types always have an e#ect
in
/* Write to x's cell */
f z;
check(!y, qc )
(a) Source program
in
f z;
check(!y, qc )
(b) Target program
C I (#x

Figure

2: Example alias and e#ect analysis
variable # on the arrow, which makes e#ect inference
easier. Notice that creating a function has no e#ect
(the potential allocation of a closure does not count as
an e#ect, because a closure cannot be updated).
. (App) applies a function to an argument. The e#ect
of applying e1 to e2 includes the e#ect # of calling the
function e1 represents. Notice that e1 's argument type
is constrained to be equal to the type of e2 . As before,
this forces possibly-aliased locations to have the same
abstract location.
. (Assert) and (Check) are translated unchanged into
the target language. Qualifiers are flow-sensitive, so
we do not model them during this first, flow-insensitive
step of the algorithm.
. (Down) hides e#ects on purely local state. If evaluating
e produces an e#ect on some location # neither in #
nor in t, then # cannot be accessed in subsequent com-
putation. Thus we can conservatively approximate the
set of e#ects that may be visible as locs(# locs(t).
By intersecting the e#ects L with the set of e#ects
that may be visible, we increase the precision of e#ect
inference, which in turn increases the precision of flow-sensitive
type qualifier inference. Although (Down) is
not a syntactic rule, it only needs to be applied once
per function body [15].

Figure

2 shows an example program and its translation.
We use some syntactic sugar; all of these constructs can be
encoded in our language (e.g., by assuming a primitive Y
combinator of the appropriate type). In this example the
constant qualifiers qa , q b , and qc are in the discrete partial
order (the qualifiers are incomparable). Just before f re-
turns, we wish to check that y has the qualifier qc . This
check succeeds only if we can model the update to y as a
strong update.
In

Figure

2, we assign x, y, and z distinct locations #x ,
#y , and #z , respectively. Because f is called with argument
z and our system is not polymorphic in locations, our alias
analysis requires that the types of z and w match, and thus
w is given the type ref (#z ). Finally, notice that since x and
y are purely local to the body of f , using the rule (Down)
our analysis hides all e#ects on #x and #y . The e#ect of f
is {#z} because f writes to its parameter w, which has type
ref (#z ). (More precisely, f has e#ect # where {#z} #.)
Let n be the size of the input program. Applying the
rules in Figure 1 generates a constraint system of size O(n),
using a suitable representation of locs(# locs(t) (see [15]).
Resolving the type equality constraints in the usual way with
unification takes O(n#(n)) time, where #(-) is the inverse
Ackerman's function. The remaining constraints are e#ect
constraints of the form L #. We solve these constraints
on-demand-in the next step of the algorithm we ask queries
of the form # L. We can answer all such queries for a single
location # in O(n) time [15].
3.2 Stores and Qualified Types
Next we perform flow-sensitive analysis to check the qualifier-
related annotations. In this second step of the algorithm we
take as input a program that has been decorated with types,
locations, and e#ects by the inference algorithm of Figure 1.
Throughout this step we treat the abstract locations # and
e#ects L from the first step as constants. We analyze the
input program using the extended types shown below:
# | int | ref (#) | (C, # L (C # )
| Merge(C, C # , L) | Filter(C, L)
Here qualified types # are standard types with qualifiers inserted
at every level. Qualifiers Q are either qualifier variables
#, which stand for currently unknown qualifiers, or
constant qualifiers B, specified by the user. We assume a
supplied partial order # among constant qualifiers.
The flow-sensitive analysis associates a store C with each
program point. This is in contrast to the flow-insensitive
step, which uses one global store C I to give types to loca-
tions. Function types are extended to (C, # L (C # ),
where C describes the store the function is invoked in and
describes the store when the function returns.
Each location in each store has an associated linearity #.
There are three linearities: 0 for unallocated locations, 1 for
linear locations (these admit strong updates), and # for non-linear
locations (which admit only weak updates). The three
linearities form a lattice 0 < 1 < #. Addition on linearities
is as expected: 0
A store is a vector
that assigns a type # i and a linearity # i to every abstract
location # i computed by the alias analysis. We call such a
vector a ground store. If G is a ground store, we write G(#)
for #'s type in G, and we write G lin (#) for #'s linearity in G.
Rather than explicitly associating a ground store with every
program point, we represent stores using a constraint
formalism. As the base case, we model an unknown store
using a store variable #. We relate stores at consecutive
program points either with store constructors (see below),
which build new stores from old stores, or with store constraints
are generated at branches from the
program point represented by store C1 to the program point
represented by store C2 .
A solution to a system of store constraints is a mapping
from store variables to ground stores, and from Assign(- )
stores (see below) to types. A solution S satisfies a system
of store constraints if for each constraint C1 # C2 we have
(Ref#

Figure

3: Store compatibility rules
according to the rules in Figure 3, and the
solution satisfies the rules in Figure 4.
In

Figure

3, constraints between stores yield constraints
between linearities and types, which in turn yield constraints
between qualifiers and between stores. In our constraint
resolution algorithm, we exploit the fact that we are only
interested in qualifier relationships to solve as little of the
expensive store constraints as possible (see Section 3.4).
In (Ref# ) we require that the locations on the left- and
right-hand sides of the # are the same. Alias analysis enforces
this property, which corresponds to the standard requirement
that subtyping becomes equality below a pointer
constructor. We emphasize that in this step we treat abstract
locations # as constants, and we will never attempt
(or need) to unify two distinct locations to satisfy (Ref# ).
In (Fun# ) we require that the e#ects of the constrained
function types match exactly. It would also be sound to
allow the e#ect of the left-hand function to be a subset of
the e#ect of the right-hand function.

Figure

4 formalizes the four kinds of store constructors by
showing how a solution S behaves on constructed stores.
The store Alloc(C, #) is the same as store C, except that
location # has been allocated once more. Allocating location
# does not a#ect the types in the store but increases the
linearity of location # by one.
The store Merge(C, C # , L) combines stores C and C # according
to e#ect L. If # L, then Merge(C, C # , L) assigns
# the type it has in C, otherwise Merge(C, C # , L) assigns #
the type it has in C # . The linearity definition is similar.
The store Filter(C, L) assigns the same types and linearities
as C for all locations # such that # L. The types of
all other locations are undefined, and the linearities of all
other locations are 0.
Finally, the store Assign(C, # ) is the same as store C,
except location # has been updated to type # where #
(we allow a subtyping step here). If # is non-linear in C, then
in

Figure

4(c) we require that the type of # in Assign(C, # :
# ) be at least the type of # in C; this corresponds to a weak
update. (In our implementation we require equality here.)
Putting these together, intuitively if # is linear then its type
in Assign(C, #) is # , otherwise its type is # S(C)(#),
where # is the least-upper bound.
3.3 Flow-Sensitive Constraint Generation

Figure

5 gives the type inference rules for our system.
In this system judgments have the form #, C
meaning that in type environment # and with initial store
(a) Types
lin (#) otherwise
lin (# L
lin (# L
(b) Linearities
lin (# S(C)(# S(Assign(C, #)
for all stores Assign(C, #)
(c) Weak updates

Figure

4: Extending a solution to constructed stores
evaluating e yields a result of type # and a new store C # .
We write C(#) for the type associated with # in store C;
we discuss the computation of C(#) in Section 3.4. We use
the function sp(t) to decorate a standard type t with fresh
qualifier and store variables:
We briefly discuss the rules in Figure 5:
. (Var) and (Int) are standard. For (Int), we pick a fresh
qualifier variable # to annotate n's type.
. (Ref) adds a location # to the store C # , yielding the
store Alloc(C #). The type # of e is constrained to be
compatible with #'s type in C # . 2
. (Deref) looks up the type of e's location # in the current
store C # . In this rule, any qualifier may appear
on e's type; qualifiers are checked only by (Check), see
below.
. (Assign) produces a new store representing the assignment
of type # to location #.
. (Lam) type checks function body e in fresh initial store
# and with parameter x bound to a type with fresh
qualifier variables.
An alternative formulation is to track the type # of e as
part of the constructed store Alloc(-), and only constrain
# to be compatible with C #) if after the allocation # is
non-linear.
#, C
#, C
#, C
#, C # ref
(Ref)
#, C
#,
(Deref)
#,
#, C # e1
#,
#,
#, C # e1
(App)
#, C
#, C # assert(e,
#, C
#, C # check(e,

Figure

5: Constraint generation rules
. (App) constrains #2 # to ensure that e2 's type is
compatible with e1 's argument type. The constraint
ensures that the current state of the
locations that e1 uses, which are captured by its e#ect
set L, is compatible with the state function e1 expects.
The final store Merge(# , C # , L) joins the store C # before
the function call with the result store # of the
function. Intuitively, this rule gives us some low-cost
polymorphism, in which functions do not act as join
points for locations they do not use.
. (Assert) adds a qualifier annotation to the program,
and (Check) checks that the inferred top-level qualifier
of e is compatible with the expected qualifier Q.

Figure

6 shows the stores and store constraints generated
for our example program. We have slightly simplified the
graph for clarity. Here # is f 's initial store and # is f 's final
store. We use undirected edges for store constructors and a
directed edge from C1 to C2 for the constraint C1 # C2 .
We step through constraint generation. We model the allocation
of #x with the store Alloc(#x ). Location #x is initialized
to 0, which is given the type #0 int for fresh qualifier
variable #0 . (Ref) generates the constraint #0 int #x)
to require that the type of 0 be compatible with #x ). We
model the allocation and initialization of #y and #z sim-
ilarly. Then we construct three Assign stores to represent
the assignment statements. We give 3 and 4 the types #3 int
and #4 int, respectively, where #3 and #4 are fresh qualifier
variables.
For the recursive call to f , we construct a Filter and add a
constraint on #. The Merge store represents the state when
the recursive call to f returns. We join the two branches of
Merge
Filter
Assign
Assign
#y :qc int
Assign
#z :#4 int
Alloc
#x :#3 int
Alloc
#z
Alloc
#y
#x
qa int # Alloc(#x )(#y )

Figure

Store constraints for example
the conditional by making edges to # . Notice the cycle, due
to recursion, in which state from # can flow to the Merge,
which in turn can flow to # . Finally, the qualifier check
requires that #y ) has qualifier qc .
3.4 Flow-Sensitive Constraint Resolution
The rules of Figure 5 generate three kinds of constraints:
qualifier constraints Q # Q # , subtyping constraints # ,
and store constraints C # (the right-hand side of a store
constraint is always a store variable). A set of m type and
qualifier constraints can be solved in O(m) time using well-known
techniques [16, 23], so in this section we focus on
computing a solution S to a set of store constraints.
Our analysis is most precise if as few locations as possible
are non-linear. Recall that linearities naturally form
a partial order 0 < 1 < #. Thus, given a set of constructed
stores and store constraints, we perform a least
fixpoint computation to determine S(C) lin (#). We initially
assume that in every store, location # has linearity 0. Then
we exhaustively apply the rules in Figure 4(b) and the rule
S(#) lin we reach a fix-
point. This last rule is derived from Figure 3.
In our implementation, we compute S(C) lin (#) in a single
pass over the store constraints using Tarjan's strongly-connected
components algorithm to find cycles in the store
constraint graph. For each such cycle containing more than
one allocation of the same location # we set the linearity of
# to # in all stores on the cycle.
Given this algorithm to compute S(C) lin (#), in principle
we can then solve the implied typing constraints using the
following simple procedure. For each store variable #, initialize
S(#) to a map
{#1 :sp(CI (#1)), . , #n :sp(CI (#n))}
and for each store Assign(C, # ) initialize
#) to sp(CI (#)), thereby assigning fresh qualifiers to the
type of every location at every program point. Replace uses
of C(#) in

Figure

5 with S(C)(#), using the logic in Figure
4(a).
Apply the following two closure rules until no more constraints
are generated:
lin (# S(C)(# S(Assign(C, #)
for all stores Assign(C, # )
Given a program of size n, in the worst case this naive algorithm
requires at least n 2 space and time to build S(-)
and generate the necessary type constraints. This cost is
too high for all but small examples. We reduce this cost in
practice by taking advantage of several observations.
Many locations are flow-insensitive. If a location # never
appears on the left-hand side of an assignment, then #'s type
cannot change. Thus we can give # one global type instead of
one type per program point. In imperative languages such as
C, C++, and Java, function parameters are a major source
of flow-insensitive locations. In these languages, because
parameters are l-values, they have an associated memory
location that is initialized but then often never subsequently
changed.
Adding extra store variables trades space for time. To
compute S(C)(#) for a constructed store C, we must deconstruct
recursively until we reach a variable store or an
assignment to # (see Figure 4(a)). Because we represent the
e#ect constraints compactly (in linear space), deconstructing
Filter(-, L) or Merge(-, L) may require a potentially linear
time computation to check whether # L. We recover
e#cient lookups by replacing C with a fresh store variable
# and adding the constraint C #. Then rather than computing
S(C)(#) we compute S(#), which requires only a
map lookup. Of course, we must use space to store # in
S(#). However, as shown below, we often can avoid this
cost completely. We apply this transformation to each store
constructed during constraint inference.
Not every store needs every location. Rather than assuming
S(#) contains all locations, we add needed locations
lazily. We add a location # to S(#) the first time the analysis
requests #) and whenever there is a constraint C # or
# C such that # S(C). Stores constructed with Filter
and Merge will tend to stop propagation of locations, saving
space (e.g., if Filter(C, L) # S(#), but # L, then we
do not propagate # to C).
We can extend this idea further. For each qualifier variable
#, inference maintains a set of possible qualifier constants
that are valid solutions for #. If that set contains
every constant qualifier, then # is uninteresting (i.e., # is
constrained only by other qualifier variables), otherwise #
is interesting. A type # is interesting if any qualifier in #
is interesting, otherwise # is uninteresting. We then modify
the closure rules as follows:
for all # S(C) or S(#) s.t.
S(C)(#) or S(#) interesting
lin (# S(C)(# S(Assign(C, #)
for all Assign(C, # ) s.t. S(C)(#) or
S(Assign(C, #) interesting
In this way, if a location # is bound to an uninteresting type,
then we need not propagate # through the constraint graph.

Figure

7 gives an algorithm for lazy location propagation.
We associate a mark with each # in each S(#) and with #
in Assign(C, # ). Initially this mark is not set, indicating
that location # is bound to an uninteresting type.
If a qualifier variable # appears in S(#), we associate
the pair (#) with #, and similarly for Assign stores. If
during constraint resolution the set of possible solutions of
# changes, we call Propagate(#,C) to propagate #, and in
turn #, through the store constraint graph.
If Propagate(#, C) is called and # is already marked in C,
we do nothing. Otherwise, Back-prop() and Forward-prop()
make appropriate constraints between S(C)(#) and S(C #)
for every store C # reachable from C. This step may add #
to C # if C # is a store variable, and the type constraints that
Back-prop() and Forward-prop() generate may trigger
subsequent calls to Propagate().
Consider again our running example. Figure 8 shows how
locations and qualifiers propagate through the store constraint
graph. Dotted edges in this graph indicate inferred
constraints (discussed below). For clarity we have omitted
the Alloc edges (summarized with a dashed line) and the
base types.
The four type constraints in Figure 6 are shown as directed
edges in Figure 8. For example, the constraint #0 int #
#x) reduces to the constraint #0 #x , which is a directed
edge #0 #x . Adding this constraint does not cause any
propagation; this constraint is among variables. Notice that
the assignment of type #3 int to #x also does not cause any
propagation.
The constraint qa int # Alloc(#x )(#y ) reduces to qa int #
#y ), which reduces to qa #y . This constraint does trigger
propagation. Propagate(#y , #) first pushes #y backward to
the Filter store. But since #y # L, propagation stops. Next
we push #y forward through the graph and stop when we
reach the store Assign(-, #y : qc int); forward propagation
assumes that this is a strong update.
contains an interesting type,
#y is propagated from this store forward through the graph.
On one path, propagation stops at the Filter. The other
paths yield a constraint qc # y . Notice that the constraint
remains satisfiable.
The constraint q b #z triggers a propagation step as
before. However, this time #z # L, and during backward
propagation when we reach Filter we must continue. Eventually
we reach Assign(-, #z : #4 int) and add the constraint
#4 #z . This in turn triggers propagation from
This propagation step reaches # ,
adds #z to S(# ), and generates the constraint #4 # z .
Finally, we determine that in the Assign stores #x and #y
are linear and #z is non-linear. (The linearity computation
uses the Alloc(-) stores, which are not shown.) Thus the
update to #z is a weak update, which yields a constraint
#z #4 .
This example illustrates three kinds of propagation. The
location #x is never interesting, so it is not propagated through
the graph. The location #y is propagated, but propagation
stops at the strong update to #y and also at the Filter, because
the (Down) rule in Figure 1 was able to prove that
#y is purely local to f . The location #z , on the other hand,
is not purely local to f , and thus all instances of #z are
conflated, and #z admits only weak updates.
case C of
#:
I (#)) to S(#) if not already in S(#)
if # is not marked in #
mark # in S(#)
Forward-prop(C, #, S(#))
for each C # such that C #
Back-prop(C #, S(#))
if # is not marked in Assign(C #)
mark # in Assign(C #)
Forward-prop(C, #)
case C of
#:
I (#)) to S(#) if not already in S(#)
Alloc(C #
Back-prop(C #)
then Back-prop(C #)
else Back-prop(C #)
then Back-prop(C #)
then #
else Back-prop(C #)
for each # such that C #
I (#)) to S(#) if not already in S(#)
for each C # such that C # is constructed from C
case C # of
Alloc(C, #
if # L and
then Forward-prop(C #)
if # L and
then Forward-prop(C #)
Filter(C,
then Forward-prop(C #)
Assign(C, #
then Forward-prop(C #)

Figure

7: Lazy location constraint propagation
4. RESTRICT
As mentioned in the introduction, type inference may fail
because a location on which a strong update is needed may
be non-linear. In practice a major source of non-linear locations
is data structures. For example, given a linked list
l, our alias analysis often cannot distinguish l->lock from
l->next->lock, hence both will likely be non-linear.
Our solution to this problem is to add a new form
restrict x =e1 in e2
to the language. Intuitively, this declares that of all aliases
of e1 , only x and copies derived from x will be used within
qc Merge
{#y :# y ,
#z :# z } # Filter
Assign
Assign
#y :qc
Assign
#z :#4
#x :#3
#x :#x , #y :#y , #z :#z }
qa

Figure

8: Constraint propagation
e2 . For example, consider
restrict {
x := .; /* valid */
y := .; /* invalid */
The first assignment through x is valid, but the assignment
through y is forbidden by restrict.
We check restrict using the following type rule, which
is integrated into the first inference pass of Figure 1:
restrict x =e1 in e2 #
restrict # x =e # 1 in e
(Restrict)
Here we bind x to a type with a fresh abstract location #
to distinguish dereferences of x from dereferences of other
aliases of e1 . The constraint # L2 forbids location # from
being dereferenced in e2 ; notice dereferences of # within
e2 are allowed. We require that # not escape the scope of
e2 with # locs(# locs(CI (# locs(t2 ), and we also
add # to the e#ect set. We translate restrict into the
target language by annotating it with the location # that
x is bound to. A full discussion of restrict, including a
soundness proof, can be found in a technical report [15].
We use restrict to locally recover strong updates. The
key observation is that the location # of e1 and the location
# of x can be di#erent. Thus even if the linearity of # is #,
the linearity of # can be 1. Therefore within the body of e2
we may be able to perform strong updates of # . When the
scope of restrict ends, we may need to do a weak update
from # to #.
For example, suppose that we wish to type check a state
change of some lock deep within a data structure, and the location
of the lock is non-linear. The following is not atypical
of Linux kernel code:
. /* non-linear loc */
Assuming the type system determines that the . above
contains no accesses to aliases of the lock and does not alias
the lock to a non-linear location, we can modify the code to
type check as follows:
restrict lock = &a->b[c].d->lock in {
In our flow-sensitive step, we use the following inference
rule for restrict:
#,
#, C # restrict # x =e1 in e2 : #2 ,
(Restrict)
In this rule, we infer a type for e1 , which is a pointer to
some location #. Then we create a new store C # in which the
location # of x is both allocated and initialized to C #). In
added to the type environment, we evaluate
e2 . Finally, the result store is the store C # with a potentially
update assigning the contents of # to #.
5. EXPERIMENTS
To test our ideas in practice we have built a tool Cqual
that implements our inference algorithm. To use Cqual,
programmers annotate their C programs with type quali-
fiers, which are added to the C syntax in the same way as
const [16]. The tool Cqual can analyze a single file or a
whole program. As is standard in type-based analysis, when
analyzing a single file, the programmer supplies type signatures
for any external functions or variables.
We have used Cqual to check two program properties:
locking in the 2.4.9 Linux kernel device drivers and uses
of the C stream library. Our implementation is sound up
to the unsafe features of C: type casts, variable-argument
functions, and ill-defined pointer arithmetic. We currently
make no attempt to track the e#ect of any of these features
on aliasing, except for the special case of type casting the
result of malloc-like functions. In combination with a system
for enforcing memory safety, such as CCured [21], our
implementation would be sound.
In our implementation, we do not allow strong updates
on locations containing functions. This improves e#ciency
because we never need to recompute S(C) lin (#)-weak updates
will not add constraints between stores. Additionally,
observe that allocations a#ect linearities but not types, and
reads and writes a#ect types but not linearities. Thus in our
implementation we also improve the precision of the analysis
by distinguishing read, write, and allocation e#ects. We
omit details due to space constraints.
The analysis results are presented to the user with an
emacs-based user interface. The source code is colored according
to the inferred qualifiers. Type errors are hyper-linked
to the source line at which the error first occurred,
and the user can click on qualifiers to view a path through
the constraint graph that shows why a type error was de-
tected. We have found the ability to visualize constraint
solutions in terms of the original source syntax not just use-
ful, but essential, to understanding the results of inference.
More detail on the ideas in the user interface can be found
in [24].
5.1 Linux Kernel Locking
The Linux kernel includes two primitive locking functions,
which are used extensively by device drivers:
void spin_lock(spinlock_t *lock);
void spin_unlock(spinlock_t *lock);
We use three qualifiers locked, unlocked, and # (unknown)
to check locking behavior. The subtyping relation is locked <
# and unlocked < #. We assign spin lock the type
(C, ref (#} (Assign(C, # : locked spinlock
where
unlocked spinlock t
We omit the function qualifier since it is irrelevant. The type
of spin lock requires that the lock passed as the argument
be unlocked (see the where clause) and changes it to locked
upon returning. The signature for spin unlock is the same
with locked and unlocked exchanged.
In practice we give spin lock this type signature by supplying
Cqual with the following definition:
void spin_lock($unlocked spinlock_t *lock) {
$locked spinlock_t);
Here change type(x, t) is just like the assignment
#something of type t#;
except that rather than give an explicit right-hand side we
just give the type of the right-hand side. In this case the
programmer needs to supply the body of spin lock because
it is inline assembly code.
Since our implementation currently lacks parametric poly-
morphism, we inline calls to spin lock and spin unlock.
Using these type signatures we can check for three kinds
of errors: deadlocks from acquiring a lock already held by
the same thread, attempts to release a lock already released
by the same thread, and attempting to acquire or release a
lock in an unknown (#) state.
We analyzed 513 whole device driver modules (a whole
module includes all the files that make up a single driver).
A module must meet a well-specified kernel interface, which
we model with a main function that non-deterministically
calls all possible driver functions registered with the kernel.
We also separately analyzed each of the 892 driver files
making up the whole modules. In these experiments we
removed the # qualifier so that locked and unlocked are
incomparable, and we made optimistic assumptions about
the environment in which each file is invoked.
We examined the results for 64 of the 513 whole device
driver modules and for all of the 892 separately analyzed
driver files. We found 14 apparently new locking bugs, including
one which spans multiple files. In five of the apparent
bugs a function tries to acquire a lock already held by
a function above it in the call chain, leading to a deadlock.
For example, the emu10k1 module contains a deadlock (we
omit the void return
emu10k1_mute_irqhandler(struct emu10k1_card *card) {
struct patch_manager
. spin_lock_irqsave(&mgr->lock, flags);
emu10k1_set_oss_vol(card, .
emu10k1_set_oss_vol(struct emu10k1_card *card, .) {
. emu10k1_set_volume_gpr(card, .
emu10k1_set_volume_gpr(struct emu10k1_card *card, .) {
struct patch_manager
. spin_lock_irqsave(&mgr->lock, flags); .
Note that detecting this error requires interprocedural analysis

One of our goals is to understand how often, and why,
our system fails to type check real programs. We have categorized
every type error in the separate file analysis of the
driver files. In this experiment, of the 52 files that fail
to type check, 11 files have locking bugs (sometimes more
than one) and the remaining 41 files have type errors. Half
of these type errors are due to incorrect assumptions about
the interface for functions; these type errors are eliminated
by moving to whole module analysis. The remaining type
errors fall into two main categories.
In many cases the problem is that our alias analysis is not
strong enough to type check the program. Another common
class of type errors arises when locks are conditionally
acquired and released. In this case, a lock is acquired if a
predicate P is true. Before the lock is released, P is tested
again to check whether the lock is held. Our system is not
path sensitive, and our tool signals a type error at the point
where the path on which the lock is acquired joins with the
path on which the lock is not acquired (since we did not
use # in these single file experiments-in the whole module
analysis, this error is detected later on, when there is an attempt
to acquire or release the lock in the # state). Most of
these examples could be rewritten with little e#ort to pass
our type system. In our opinion, this would usually make
the code clearer and safer-the duplication of the test on P
invites new bugs when the program is modified.
Even after further improvements, we expect some dynamically
correct programs will not type check. As future work,
we propose the following solution. The qualifier # represents
an unknown state. We can use the information in the
constraints to automatically insert coercions to and from #
where needed. During execution these coercions perform
runtime tests to verify locks are in the correct state. Thus,
our approach can introduce dynamic type checking in situations
where we cannot prove safety statically.
Of the 513 whole modules, 196 contain type errors, many
of which are duplicates from shared code. We examined 64
of the type error-containing modules and discovered that a
major source of type errors is when there are multiple aliases
of a location, but only one alias is actually used in the code
of interest. Not surprisingly, larger programs, such as whole
modules, have more problems with spurious aliasing than
the optimistic single-file analysis. We added restrict annotations
by hand to the 64 modules we looked at, including
the emu10k1 module, which yielded the largest number of
such false positives. Using restrict, we eliminated all of
the false positives in these modules that occurred because
non-linear locations could not be strongly updated. This
supports our belief that restrict is the right tool for dealing
with (necessarily) conservative alias analysis. Currently
adding restrict by hand is burdensome, requiring a relatively
large number of annotations. We leave the problem
of automatically inferring restrict annotations as future
work.
5.2 C Stream Library
As mentioned in the introduction, the C stream library
0k 100k 200k 300k 400k 500k 600k 700k 800k
Size (preprocessed lines of code)
Time
(sec)
Flow sensitive Flow insensitive Parsing1003005007009000k 100k 200k 300k 400k 500k 600k 700k 800k
Size (preprocessed lines of code)
Space
(Mbytes)

Figure

9: Resource usage for whole module analysis
interface contains certain sequencing constraints. For ex-
ample, a file must be opened for reading before being read.
A special property of the C stream library is that the result
of fopen must be tested against NULL before being used, because
fopen may or may not succeed. The class of C stream
library usage errors our tool can detect includes files used
without having been opened and checked against NULL, files
opened and then accessed in an incompatible mode, and files
accessed after being closed. We omit the details due to space
constraints.
We tried our tool on two application programs, man-1.5h1
and sendmail-8.11.6. We were primarily interested in the
performance of our tool on a more complex application (see
below), as we did not expect to find any latent stream library
usage bugs in such mature programs. However, we did find
one minor bug in sendmail, in which an opened log file is
never closed in some circumstances.
5.3 Precision and Efficiency
The algorithm described in Section 3.4 is carefully designed
to limit resource usage. Figure 9 shows time and
space usage of whole module analysis versus preprocessed
lines of code for 513 Linux kernel modules. All experiments
were done on a dual processor 550 MHz Pentium III with
2GB of memory running RedHat 6.2.
We divide the resource usage into C parsing and type
checking, flow-insensitive analysis, and flow-sensitive analy-
sis. Flow-insensitive analysis consists of the alias and e#ect
inference of Figure 1 together with flow-insensitive qualifier
inference [16]. Flow-sensitive analysis consists of the constraint
generation and resolution described in Sections 3.3-
3.4, including the linearity computation. In the graphs, the
reported time and space for each phase includes the time
and space for the previous phases.
The graphs show that the space overhead of flow-sensitive
analysis is relatively small and appears to scale well to large
modules. For all modules the space usage for the flow-sensitive
analysis is within 31% of the space usage for the
flow-insensitive analysis. The running time of the analysis
is more variable, but the absolute running times are within
a factor of 1.3 of the flow-insensitive running times.
The analysis of sendmail-8.11.6, with 175,193 preprocessed
source lines, took 28.8 seconds and 264MB; man-1.5h1,
with 16,411 preprocessed source lines, took 1.85 seconds and
32MB. These results suggest that our algorithm also behaves
e#ciently when checking C stream library usage.
6. CONCLUSION
We have presented a system for extending standard type
systems with flow-sensitive type qualifiers. We have given
a lazy constraint resolution algorithm to infer type qualifier
annotations and have shown that our analysis is e#ective
in practice by finding a number of new locking bugs in the
7.



--R


Better Static Memory Management: Improving Region-Based Analysis of Higher-Order Languages
An Extended Form of Must Alias Analysis for Dynamic Allocation.
Analysis of Pointers and Structures.
Typed Memory Management in a Calculus of Capabilities.

Enforcing High-Level Protocols in Low-Level Software

Checking System Rules Using System-Specific
Bugs as Deviant Behavior: A General Approach to Inferring Errors in Systems Code.
Static Detection of Dynamic Memory Errors.
Adoption and Focus: Practical Linear Types for Imperative Programming.

Extended Static Checking for Java.
Checking Programmer-Specified Non-Aliasing
A Theory of Type Qualifiers.
Cyclone user's manual.
Resource Usage Analysis.



A Simple
Tractable Constraints in Finite Semilattices.
Detecting Format String Vulnerabilities with Type Qualifiers.
Alias Types.
A Type System for Java Bytecode Subroutines.
A Programming Language Concept for Enhancing Software Reliability.
Implementation of the Typed Call-by-Value #-Calculus using a Stack of Regions
Alias Types for Recursive Data Structures.
Personal communication.

Typing References by E
Typestate Checking of Machine Code.
--TR
Compilers: principles, techniques, and tools
Typestate: A programming language concept for enhancing software reliability
Polymorphic effect systems
Analysis of pointers and structures
Typing references by effect inference
Implementation of the typed call-by-value MYAMPERSAND#955;-calculus using a stack of regions
Context-sensitive interprocedural points-to analysis in the presence of function pointers
An extended form of must alias analysis for dynamic allocation
Efficient context-sensitive pointer analysis for C programs
Better static memory management
Static detection of dynamic memory errors
A type system for Java bytecode subroutines
Single and loving it
A simple, comprehensive type system for Java bytecode subroutines
Typed memory management in a calculus of capabilities
A theory of type qualifiers
Type-based race detection for Java
Enforcing high-level protocols in low-level software
Bugs as deviant behavior
CCured
Resource usage analysis
Adoption and focus
Extended static checking for Java
Alias Types
Typestate Checking of Machine Code
Tractable Constraints in Finite Semilattices
Alias Types for Recursive Data Structures
Cyclone User''''s Manual, Version 0.1.3
Checking Programmer-Specified Non-Aliasing

--CTR
David Greenfieldboyce , Jeffrey S. Foster, Visualizing type qualifier inference with Eclipse, Proceedings of the 2004 OOPSLA workshop on eclipse technology eXchange, p.57-61, October 24-24, 2004, Vancouver, British Columbia, Canada
Futoshi Iwama , Naoki Kobayashi, A new type system for JVM lock primitives, Proceedings of the ASIAN symposium on Partial evaluation and semantics-based program manipulation, p.71-82, September 12-14, 2002, Aizu, Japan
Gary Wassermann , Zhendong Su, Sound and precise analysis of web applications for injection vulnerabilities, ACM SIGPLAN Notices, v.42 n.6, June 2007
Brian Chess , Gary McGraw, Static Analysis for Security, IEEE Security and Privacy, v.2 n.6, p.76-79, November 2004
Vincent Simonet, An extension of HM(X) with bounded existential and universal data-types, ACM SIGPLAN Notices, v.38 n.9, p.39-50, September
Timothy Fraser , Nick L. Petroni, Jr. , William A. Arbaugh, Applying flow-sensitive CQUAL to verify MINIX authorization check placement: 3, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada
Futoshi Iwama , Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis for a functional language with exceptions, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina
Ranjit Jhala , Rupak Majumdar, Bit level types for high level reasoning, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA
David Koes , Mihai Budiu , Girish Venkataramani, Programmer specified pointer independence, Proceedings of the 2004 workshop on Memory system performance, June 08-08, 2004, Washington, D.C.
Benjamin Chelf , Dawson Engler , Seth Hallem, How to write system-specific, static checkers in metal, ACM SIGSOFT Software Engineering Notes, v.28 n.1, p.51-60, January
Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Permissive interfaces, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
Yanhong A. Liu , Tom Rothamel , Fuxiang Yu , Scott D. Stoller , Nanjun Hu, Parametric regular path queries, ACM SIGPLAN Notices, v.39 n.6, May 2004
Yoann Padioleau , Julia L. Lawall , Gilles Muller, Understanding collateral evolution in Linux device drivers, ACM SIGOPS Operating Systems Review, v.40 n.4, October 2006
Eran Yahav , G. Ramalingam, Verifying safety properties using separation and heterogeneous abstractions, ACM SIGPLAN Notices, v.39 n.6, May 2004
Samuel Z. Guyer , Calvin Lin, Error checking with client-driven pointer analysis, Science of Computer Programming, v.58 n.1-2, p.83-114, October 2005
Junfeng Yang , Ted Kremenek , Yichen Xie , Dawson Engler, MECA: an extensible, expressive system and language for statically checking security properties, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA
Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, ACM SIGPLAN Notices, v.40 n.1, p.351-363, January 2005
Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.264-313, March 2005
Naoki Kobayashi, Time regions and effects for resource usage analysis, ACM SIGPLAN Notices, v.38 n.3, March
Atsushi Igarashi , Naoki Kobayashi, A generic type system for the Pi-calculus, Theoretical Computer Science, v.311 n.1-3, p.121-163, 23 January 2004
J. Field , D. Goyal , G. Ramalingam , E. Yahav, Typestate verification: abstraction techniques and complexity results, Science of Computer Programming, v.58 n.1-2, p.57-82, October 2005
system for resource protocol verification and its correctness proof, Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.135-146, August 24-25, 2004, Verona, Italy
Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, ACM SIGPLAN Notices, v.38 n.9, p.213-225, September
Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Certified In-lined Reference Monitoring on .NET, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada
Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, ACM SIGPLAN Notices, v.37 n.5, May 2002
Ranjit Jhala , Rupak Majumdar, Path slicing, ACM SIGPLAN Notices, v.40 n.6, June 2005
Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, ACM SIGPLAN Notices, v.39 n.1, p.232-244, January 2004
Yichen Xie , Alex Aiken, Saturn: A scalable framework for error detection using Boolean satisfiability, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.3, p.16-es, May 2007
Alex Aiken , Jeffrey S. Foster , John Kodumal , Tachio Terauchi, Checking and inferring local non-aliasing, ACM SIGPLAN Notices, v.38 n.5, May
Adrian Birka , Michael D. Ernst, A practical type system and language for reference immutability, ACM SIGPLAN Notices, v.39 n.10, October 2004
Christian Skalka, Trace effects and object orientation, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.139-150, July 11-13, 2005, Lisbon, Portugal
Nurit Dor , Stephen Adams , Manuvir Das , Zhe Yang, Software validation via scalable path-sensitive value flow analysis, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
Ted Kremenek , Ken Ashcraft , Junfeng Yang , Dawson Engler, Correlation exploitation in error ranking, ACM SIGSOFT Software Engineering Notes, v.29 n.6, November 2004
Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, Proceedings of the 6th conference on Symposium on Opearting Systems Design & Implementation, p.19-19, December 06-08, 2004, San Francisco, CA
Murali Krishna Ramanathan , Ananth Grama , Suresh Jagannathan, Static specification inference using predicate mining, ACM SIGPLAN Notices, v.42 n.6, June 2007
Wei-Ngan Chin , Siau-Cheng Khoo , Shengchao Qin , Corneliu Popeea , Huu Hai Nguyen, Verifying safety policies with size properties and alias controls, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
Polyvios Pratikakis , Jaime Spacco , Michael Hicks, Transparent proxies for java futures, ACM SIGPLAN Notices, v.39 n.10, October 2004
Jeffrey Fischer , Ranjit Jhala , Rupak Majumdar, Joining dataflow with predicates, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
Karl Chen , David Wagner, Large-scale analysis of format string vulnerabilities in Debian Linux, Proceedings of the 2007 workshop on Programming languages and analysis for security, June 14-14, 2007, San Diego, California, USA
Matthew S. Tschantz , Michael D. Ernst, Javari: adding reference immutability to Java, ACM SIGPLAN Notices, v.40 n.10, October 2005
Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, ACM Transactions on Computer Systems (TOCS), v.24 n.4, p.393-423, November 2006
Madanlal Musuvathi , Dawson R. Engler, Model checking large network protocol implementations, Proceedings of the 1st conference on Symposium on Networked Systems Design and Implementation, p.12-12, March 29-31, 2004, San Francisco, California
Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, ACM SIGPLAN Notices, v.37 n.5, May 2002
Nic Volanschi, Condate: a proto-language at the confluence between checking and compiling, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy
Gregor Snelting , Torsten Robschink , Jens Krinke, Efficient path conditions in dependence graphs for software safety analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.15 n.4, p.410-457, October 2006
Tian Zhao , Jens Palsberg , Jan Vitek, Type-based confinement, Journal of Functional Programming, v.16 n.1, p.83-128, January 2006
Brian Chin , Shane Markstrum , Todd Millstein, Semantic type qualifiers, ACM SIGPLAN Notices, v.40 n.6, June 2005
Polyvios Pratikakis , Jeffrey S. Foster , Michael Hicks, LOCKSMITH: context-sensitive correlation analysis for race detection, ACM SIGPLAN Notices, v.41 n.6, June 2006
Xiaolan Zhang , Larry Koved , Marco Pistoia , Sam Weber , Trent Jaeger , Guillaume Marceau , Liangzhao Zeng, The case for analysis preserving language transformation, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
Todd Millstein, Practical predicate dispatch, ACM SIGPLAN Notices, v.39 n.10, October 2004
Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , Dawson R. Engler, EXE: automatically generating inputs of death, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA
John Tang Boyland , William Retert, Connecting effects and uniqueness with adoption, ACM SIGPLAN Notices, v.40 n.1, p.283-295, January 2005
David Hovemeyer , William Pugh, Finding bugs is easy, ACM SIGPLAN Notices, v.39 n.12, December 2004
Philip W. L. Fong, Pluggable verification modules: an extensible protection mechanism for the JVM, ACM SIGPLAN Notices, v.39 n.10, October 2004
Yao-Wen Huang , Fang Yu , Christian Hang , Chung-Hung Tsai , Der-Tsai Lee , Sy-Yen Kuo, Securing web application code by static analysis and runtime protection, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA
Chris Andreae , James Noble , Shane Markstrum , Todd Millstein, A framework for implementing pluggable type systems, ACM SIGPLAN Notices, v.41 n.10, October 2006
Jeffrey S. Foster , Robert Johnson , John Kodumal , Alex Aiken, Flow-insensitive type qualifiers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1035-1087, November 2006
M. Pistoia , S. Chandra , S. J. Fink , E. Yahav, A survey of static analysis methods for identifying security vulnerabilities in software systems, IBM Systems Journal, v.46 n.2, p.265-288, April 2007
M. Pistoia , S. Chandra , S. J. Fink , E. Yahav, A survey of static analysis methods for identifying security vulnerabilities in software systems, IBM Systems Journal, v.46 n.2, p.265-288, April 2007
constraints;effect inference;linux kernel;restrict;locking;flow-sensitivity;type qualifiers;types;alias analysis