Arrival and Coffee: 9:30 - 10:00
Session 1: 10:00 - 11:30
Kathleen Fisher, AT&T
Typing Traits
Eduardo Bonelli (Stevens Institute of Technology)
SIFTAL: A Typed Assembly Language for Secure Information Flow Analysis
Break: 11:30 - 11:45
Session 2: 11:45 - 12:30
Chung-Chieh Shan (Harvard)
Grafting Trees: Continuations In Type Logical Grammar
Lunch: 12:30 - 1:25
Business meeting: 1:25 - 1:30
Session 3: 1:30 - 2:15
Elsa Gunter (New Jersey Institute of Technology)
Bringing Testing and Verification Closer Together
Break: 2:15 - 2:30
Session 4: 2:30 - 4:00
Vijay Saraswat (IBM T.J. Watson)
The Emergence of Systems Biology
Iliano Cervesato (NRL)
The Logical Meeting Point of Multiset Rewriting and Process Algebra
Joint work with John Reppy (University of Chicago)
Abstract: We study information flow for a typed assembly language where security types restrict information flow. Inspired by recent work in continuation-based information flow analysis, our language, Secure Information Flow TAL (SIFTAL), uses low-level linear continuations in order to impose a stack discipline on the control flow of programs. The challenge posed by studying information flow analysis at the assembly language level is many-fold. On the one hand, the well behaved control constructs of high-level languages are not available, and, on the other hand, the role of an unbounded number of variables is played by a finite number of registers that need to be reused not only with different types, but also with different security levels. Non-interference refers to the desirable property of systems of multilevel security architecture that states that information stored at a high security level does not affect computed low security level values. Our main contributions are a type system for checking that typed assembly language programs enjoy non-interference and its proof of soundness. Furthermore, SIFTAL is the first typed assembly language with security types for information flow analysis, and our proof is the first proof of non-interference for a MIPS-style typed assembly language.
This is joint work with Adriana Compagnoni and Ricardo Medel.
Abstract: Linguists strive to scientifically explain why "no student liked a course" is ambiguous, why "no student liked any course" is unambiguous, and why both of these sentences sound better than "any student liked no course". I view making a linguistic theory as specifying a programming language: one devises a type system to characterize what utterances are acceptable, and uses a denotational semantics to explain which statements are true. Following this analogy, programming language research can inform linguistic theory and vice versa.
In this talk, I illustrate this analogy with a linear logic that incorporates the notion of delimited continuations and a limited form of staging. This logic predicts the acceptability of the sentences above and delivers their readings via the formulae-as-types correspondence. In general, computational side effects are intimately related to referential opacity in natural languages. This link allows an unprecedented variety of linguistic phenomena to be uniformly analyzed.
No prior knowledge of linguistics will be assumed.
This work is joint work with Chris Barker, University of California, San Diego.
Abstract: While verification methods are becoming more frequently integrated into software development projects, software testing is still the main method used to search for programming errors. Unlike software verification techniques, software testing is usually less systematic and exhaustive. However, it is applicable even in cases where verification fails due to memory and time limitations. Testing usually is done in an informal way such as by walking through the code or inspecting the various potential pitfalls of the program [Meyer]. We present a tool for testing execution paths in sequential and concurrent programs. The tool, path exploration tool (Pet), visualizes concurrent code as flow graphs, and allows the user to interactively select an (interleaved) execution path. It then calculates and displays the condition to execute such a path, and allows the user to easily modify the selection in order to cover additional related paths.
In addition to the user selecting a path, the user may want to know if there exists any path satisfying some condition. Temporal logic [Pnueli] is often used as the specification formalism for the automatic verification of finite state systems. The automatic temporal verification of a system is a procedure that returns a yes/no answer, and in the latter case also provides a counterexample. Pet has a new application for temporal logic, as a way of assisting the debugging of a concurrent or a sequential program. We employ temporal logic over finite sequences as a constraint formalism that is used to control the way incrementally select path fragments of an execution in the system under study. In the simplest application of this ability, Pet may be used as a model checker. However, using such temporal specification and various search strategies, we are able to traverse the executions of the system and obtain important intuitive information about its behaviors. We describe the design and architecture of this tool and suggest various extensions. We also discuss the application of this tool to the design and development of an infusion pump being developed at the Walter Reid Army Institute of Research.
Abstract: The past several years have seen an emerging confluence of computer science and biology, focused on the tremendous opportunities for modeling and symbolic reasoning in biological systems. Fundamentally, one may think of the challenge at hand is to understand the normal and pathological functioning of the Biological Computer -- the intricate network of billions of cause-effect chains that make up life processes. From a computer science point of view, such work is extremely challenging because it requires the integration of discrete change (e.g. as involved in gene expression) with continuously varying phenomena (e.g. Michaelis-Menten reactions), which may possibly be stochastic in nature (e.g. using Gillespie simulation) and may need to be modeled across several orders of magnitude.
Several research groups across the world (e.g. Caltech, Harvard-MIT post-genomics Institute, Princeton, Institute for Systems Biology, U Auckland) are now starting to focus on this area. For instance, researchers are collaborating on the development of the Systems Biology Markup language [SBML], and CellML [CellML]. Several special-purpose simulators are being built for this area (e.g. Cellerator, Gepasi, JDesigner etc). Other researchers are applying ideas from constraint programming e.g. to model alternative gene splicing in HIV.
We will illustrate the basic challenges at hand with a few different examples (specifically [HIV], [Cell-Div]), and describe how our own research work on hybrid concurrent constraint programming fits into this framework.
References
[HIV] Damien Eveillard, Delphine Ropers, Hidde de jong, Christiane Branlant, Alexander Bockmayr "A multi-site constraint programming model of alternative splicing regulation", INRIA Technical Report May 2003. See http://www.loria.fr/~bockmayr
[Cell-Div]Shapiro, BE and Mjolsness "Developmental Simulations with Cellerator", Proceedings of the Second International Conference on Systems Biology, pp 342-351, 2001. See http://www-aig.jpl.nasa.gov/public/mls/cellerator/pubs.html
A Tiwari, "Automated tecniques for stability analysis of Delta-Notch Lateral Inhibition Mechanism". See http://www.csl.sri.com/users/tiwari
[CellML] http://www.cellml.org/public/about/what_is_cellml.html
[SBML] Systems Biology Workbench Development Group http://www.sbw-sbml.org/the_project.html