Refreshments and registration will be available starting at 9:30
a.m.
Preliminary Program.
| Time |
Speaker |
Title |
| 10:00 - 10:25 |
Gerald J. Holzmann,
NASA/JPL Laboratory for Reliable Software |
Limits to Growth |
| 10:25 - 10:50 |
Alex David Groce, NASA/JPL
Laboratory for Reliable Software |
Model Checking, Dynamic
Analysis, and Unsound Abstractions |
| 10:50 - 11:15 |
Annie Liu, Matt Wu,
CalTech |
Virtual Environments for
Developing Strategies for Interdicting Terrorists Carrying Dirty
Bombs |
| 11:15 - 11:40 |
Concetta Pilotto and
Sayan Mitra Caltech, Infospheres Group |
Formations of Mobile
Agents with Message Loss and Delay |
| 11:40 - 12:05 |
Jeffrey Fischer,
UCLA |
Tasks: Language Support
for Event-driven Programming |
| 12:05 - 1:30 |
|
Lunch |
| 1:30 - 1:55 |
Pat Rondon,
UC San Diego |
Liquid Types |
| 1:55 - 2:20 |
Pierre Ganty, UCLA |
Abstract fixpoint checking |
| 2:20 - 2:45 |
Ru-Gang Xu, UCLA |
Proving non-termination |
| 2:45 - 3:10 |
Daniel Marino and Todd
Millstein, UCLA |
A Theory of
Programmer-Defined Effect Systems |
| 3:10 - 3:45 |
|
Break |
| 3:45 - 4:10 |
Jacob Matthews, U. of
Chicago |
A Semantic Approach to
Multi-Language Systems |
| 4:10 - 4:35 |
Melissa O'Neill, Harvey
Mudd College |
Smarter Garbage
Collection with Simplifier |
| 4:35 - 5:00 |
Participants |
Discussion of future
meetings of SoCal |
| 5:35 - 6:15 |
James Turrell
Skyscape |
"Dividing the Light":
light show |
The list of abstracts is:
Limits to Growth --
Gerard J. Holzmann,
NASA/JPL Laboratory for Reliable Software
The ultimate goal of the use of distributed algorithms in logic model
checkers is to achieve as close as possible to an N-fold speedup on
N cpus. The best case application for these algorithms is clearly
a single multi-core or multi-cpu system with shared memory.
Experiments with a new implementation of Spin for multi-core systems
has shown that near linear speedups on relatively small multi-core
systems is feasible. Similar experiments of much larger shared
memory systems seems to indicate though that there may well be
a limit to the size of the problem-size that can be handled efficiently.
The maximum value of N (number of cpus or cores) that can effectively
run in parallel may be limited to a value that depends critically on
the structure of the state space graph itself.
I will show evidence of this effect, and discuss the longer-term
implications of these observations.
Model Checking, Dynamic Analysis, and Unsound Abstractions --
Alex David Groce,
NASA/JPL Laboratory for Reliable Software
A recent trend in software model checking is the use of model
checkers that actually execute programs. This approach has been
particularly useful in dealing with rich properties, such as functional
correctness, of actual implementation programs. Unfortunately, the state
spaces of real programs are often very large, and finding sound
abstractions for rich properties is often impossible. We discuss the use
of dynamic analysis to assist in this kind of software model checking,
especially to "manage" unsound abstractions, e.g. computing coverage and
introducing search heuristics based on structural properties to improve
abstract state-space coverage. This work is based on experience model
checking flight software at JPL.
Virtual Environments for Developing Strategies for Interdicting Terrorists
Carrying Dirty Bombs --
Annie Liu and Matt Wu,
CalTech
Strategies for detecting terrorists carrying radioactive material
can be evaluated in virtual environments more easily than they can be in
the real world. Real scenarios expose personnel to radiation and
concomitant dangers. The execution of multiple real-world scenarios - such
as catching terrorists in factories, houses and open spaces - is expensive.
This paper describes virtual environments for interdicting terrorists
carrying radioactive material. The virtual environments are constructed by
incorporating the physics of radiation into virtual-world platforms. We
explore the relative advantages of a gaming engine (Half-Life 2), a 3D
online virtual world (Second Life) and a robot simulator platform
(Stage/Player) for developing strategies for interdicting dirty bombers.
Preliminary results on implementations of these virtual environments are
presented.
Formations of Mobile Agents with Message Loss and Delay --
Concetta Pilotto and Sayan Mitra,
Caltech, Infospheres Group
This talk presents protocols for pattern formation by
sets of mobile agents that communicate by messages that may be lost,
reordered, and delayed. The patterns considered are a class of linear
polytopes that are populated by equi-spaced points. The proposed
protocols are asynchronous and distributed. The talk presents a
systematic method for proving convergence of pattern formation
protocols in this asynchronous setting by combining invariance
assertions with proofs about temporal limits of state sequences.
Tasks: Language Support for Event-driven Programming --
Jeffrey Fischer (joint work with Rupak Majumdar and Todd Millstein), UCLA
The event-driven programming style is pervasive as an efficient method
for interacting with the environment. Unfortunately, the event-driven
style severely complicates program maintenance and understanding, as
it requires each logical flow of control to be fragmented across
multiple independent callbacks.
We propose tasks as a new programming model for organizing
event-driven programs. Tasks are a variant of cooperative
multi-threading and allow each logical control flow to be modularized
in the traditional manner, including usage of standard control
mechanisms like procedures and exceptions. At the same time, by using
method annotations, task-based programs can be automatically and
modularly translated into efficient event-based code, using a form of
continuation passing style (CPS) translation. A linkable scheduler
architecture permits tasks to be used in many different contexts.
We have instantiated our model as a backward-compatible extension to
Java, called TaskJava. In this talk, I'll discuss the TaskJava
language and the implementation of the TaskJava compiler. I will also
describe in-progress work on a version for embedded systems and a
potential application of TaskJava to implement secure web
applications.
Liquid Types --
Pat Rondon,
UC San Diego
We present Logically Qualified Data Types, abbreviated to Liquid Types, a
system that combines Hindley-Milner type inference with Predicate
Abstraction to automatically infer dependent types precise enough to prove
a variety of safety properties. Liquid types allow programmers to reap
many of the benefits of dependent types, namely static verification of
critical properties and the elimination of expensive run-time checks,
without paying the heavy price of of manual annotation. We have
implemented liquid type inference in Cliq, which takes as input an Ocaml
program and a set of logical qualifiers and infers dependent types for the
expressions in the Ocaml program. To demonstrate the utility of our
approach, we describe experiments using Cliq to statically verify the
safety of array accesses on a set of challenging Ocaml benchmarks that were
previously annotated with dependent types as part of the DML project. We
show that when used in conjunction with an elementary method for
automatically generating qualifiers from program text, Cliq reduces the
amount of manual annotation required for proving safety from 31% of program
text to under 1%.
Abstract fixpoint checking --
Pierre Ganty, UCLA (joint work with Patrick Cousot and Jean-Francois Raskin)
We will present an abstract fixpoint checking algorithm with
automatic refinement by backward completion in Moore closed abstract
domains. We study the properties of our algorithm and prove it to be
more precise than the counterexample guided abstract refinement
algorithm (CEGAR). Contrary to several works in the literature, our
algorithm does not require the abstract domains to be partitions of
the state space. We also show that our automatic refinement technique
is compatible with so-called acceleration techniques. Furthermore,
the use of Boolean closed domains does not improve the precision of
our algorithm.
Proving non-termination --
Ru-Gang Xu, UCLA (joint work with Ashutosh Gupta, Tom Henzinger, Rupak Majumdar,
and Andrey Rybalchenko)
The search for proof and the search for counterexamples (bugs) are
complementary activities that need to be pursued concurrently in order to
maximize the practical success rate of verification tools. While this is
well-understood in safety verification, in liveness verification the focus,
to date, has been almost exclusively on the search for termination proofs. A
counterexample to termination is an infinite, nonterminating
programexecution. In this paper, we search for such counterexamples. The
search proceeds in two phases, by first dynamically enumerating lasso-shaped
candidate paths for counterexamples, and then statically proving their
feasibility. We illustrate the utility of our nontermination prover, TNT, on
several nontrivial examples, some of which require bit-level reasoning about
integer representations.
A Theory of Programmer-Defined Effect Systems --
Daniel Marino and Todd Millstein, UCLA
Type-and-effect systems are a natural approach for statically
reasoning about a program's execution. In addition to their use in
tracking computational effects like memory manipulation and
exceptions, type-and-effect systems can be used to reason about a
variety of application-specific properties of interest.
Unfortunately, each type-and-effect system is typically implemented as
its own monolithic type system that hard-codes a particular kind of
effects along with rules to track and control those effects. Since
language designers and researchers cannot anticipate all the useful
kinds of type-and-effect systems, it is desirable to instead allow
*programmers* to easily define their own type-and-effect systems.
Toward this end, we have developed a theory
that extracts the common core of type-and-effect systems and is
parametric in the details which distinguish the various systems.
An "instantiation" of the formalism for a particular effect
discipline is achieved by defining two functions. We have
established a simple set of lemmas that these functions must
satisfy in order for the resulting effect system to satisfy
a standard notion of soundness. We have verified our results
by encoding the theory and metatheory in the Twelf
proof assistant in the context of a simple, imperative language.
In addition, Twelf's logic programming engine allows us to
actually "run" the formal rules that compose the static and dynamic
semantics, yielding a prototype implementation of a language
with user-defined, statically-checked effects.
A Semantic Approach to Multi-Language Systems --
Jacob Matthews,
University of Chicago
Software developers have long understood that real applications are
built out of components written in different languages. Connecting
these components presents both implementation-level challenges (such
as how to resolve differences in byte layouts or memory management
schemes) and semantic-level challenges (such as what a foreign
interface does to a language's type-safety or program-equivalence
properties). The question of how to resolve implementation-level
differences has been studied extensively. By contrast, researchers have
spent little time developing insight on how to reconcile semantic
differences. In this talk I introduce a simple technique for investigating
these semantic questions by giving operational semantics to
multi-language systems in terms of the operational semantics of their
constituent languages.
Smarter Garbage Collection with Simplifiers -- Melissa O'Neill, Harvey
Mudd College
This talk introduces a method for providing lightweight daemons,
called simplifiers, that attach themselves to program data. If a data item
has a simplifier, the simplifier may be run automatically from time to
time, seeking an opportunity to ``simplify'' the object in some way that
improves the program's time or space performance. Tracing garbage
collectors can both support the simplifier abstraction and benefit from it.
Because tracing collectors traverse program data structures, they can
trigger simplifiers as part of the tracing process. Simplifiers can aid
efficient collection by simplifying objects before they are traced, thereby
eliminating some data that would otherwise have been traced and saved by
the collector. Performance data shows that appropriately chosen
simplifiers can lead to tangible space and speed benefits in practice.
All participants are invited to stay for the light display associated
with the James Turrell Skyspace, "Dividing the Light", in the Edmunds
courtyard. The show begins at sunset and continues for roughly 45 minutes,
though you can stay for as much or little as you wish.