We are studying formal methods for specifying, deriving, and reasoning about concurrent systems. First, we are developing methods for specifying and proving the equivalence of program modules in open distributed systems. Specifically, we are studying high-level linguistic abstractions to express different kinds of specifications. Second, we are investigating methods for transforming such specifications into executable concurrent code. The methods will allow manipulation of both specification components and their derived program modules. The methods will therefore provide a formal basis for modular development of open distributed software systems.

We develop algorithms and software for modeling and analyzing biomolecules as geometric entities. Think of a molecule as a union of spherical balls, one per atom. The (weighted) Voronoi cells decompose the union into closed convex pieces. The nerve of the collection of pieces is a simplicial complex. This complex is the basic data structure that allows us to compute geometric and topological properties of the molecule. The software will be extended and applied to the protein-ligand docking problem and to molecular dynamics.

Geometric modeling questions are typically studied relative to an overall approach or data structure, such as the framework of constructive solid geometry (CSG) or boundary representations, etc. The idea of representing objects by simplicial complexes is old and well developed in the area of algebraic topology. The algorithmic aspects of simplicial complexes are not well understood though. We develop techniques towards a fully general modeling system based on simplicial complexes. This system will support smooth surface representations of shapes. The central operation is the deformation of one shape into another.

This research is aimed at bridging the gap between functional and imperative programming. Imperative lambda calculus is an extension of the typed lambda calculus with new types, such as references, observers, and commands. A state-dependent computation is called an observer and commands are viewed as transformations of observers. The language has a reduction semantics and satisfies the crucial properties of Church-Rosser and strong normalization. It also has a constructive logic interpretation whereby the novel constructs can be viewed as the introduction or elimination operators for a new quantifier. Thus, impera- tive lambda calculus forms a foundation for a new synthe- sis of functional and imperative programming paradigms. Further theoretical properties of this formal system are being investigated.

We are currently investigating a variety of problems in combinatorial algorithms, including algorithms for search problems (unbounded, unimodal, bimodal, and error-prone), graph drawing, scheduling, and pursuit (discrete and continuous). We are also applying combinatorial methods to the solution of divide-and-conquer recurrence relations.

Denotes principal investigator.

Photo Caption:

Professor Lenny Pitt meets with members of his research group, Stephen Kwek (left) and Dan Oblinger. Pitt's main area of interest is computational learning theory, which approaches issues of machine learning from a formal mathematical perspective. (Photo: courtesy of the department)

Photo Caption:

Graduate researcher Bill Tolone interacts with wOrlds, a next generation computer-supported collaborative work environment. wOrlds was developed at Illinois under the direction of Professors Mehdi Harandi and Simon Kaplan. (Photo: courtesy of the department)

Photo Caption:

Graduate researcher Mike Facello works with Alpha Shapes software, a 3-D scientific visualization program based on mathematical principles of computational geometry, developed by Professor Herbert Edelsbrunner and NCSA researcher Ping Fu. (Photo: courtesy of the department)