Home

Previous years

SoCal Spring 2005

SoCal Spring 2004

SoCal Fall 2002

Call for Participation

Registration

Directions

Program

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.