Wolfgang H. Polak - Publications

This paper describes in some detail the computer-aided proof of a permutation program obtained using the Stanford Pascal verifier. We emphasize the systematic way in which a proof can be developed from an intuitive understanding of the program. The paper illustrates the current state of the art in automatic program verification.

The Stanford PASCAL verifier is an interactive program verification system. It automates much of the work necessary to analyze a program for consistency with its documentation, and to give a rigorous mathematical proof of such consistency or to pin-point areas of inconsistency. It has been shown to have applications as an aid to programming, and to have potential for development as a new and useful tool in the production of reliable software.

A method of documenting exception propagation and handling in Ada programs is proposed. Exception propagation declarations are introduced as a new component of Ada specifications. This permits documentation of those exceptions that can be propagated by a subprogram. Exception handlers are documented by entry assertions. Axioms and proof rules for Ada exceptions are given. These rules are simple extensions of previous rules for Pascal and define an axiomatic semantics of Ada exceptions. As a result, Ada programs specified according to the method can be analysed by formal proof techniques for consistency with their specifications, even if they employ exception propagation and handling to achieve required results (i.e. non-error situations). Example verifications are given.

A method of documenting exception propagation and handling in Ada programs is proposed. Exception propagation declarations are introduced as a new component of Ada specifications, permitting documentation of those exceptions that can be propagated by a subprogram. Exception handlers are documented by entry assertions. Axioms and proof rules for Ada exceptions given. These rules are simple extensions of previous rules for Pascal and define an axiomatic semantics of Ada exceptions. As a result, Ada programs specified according to the method can be analyzed by formal proof techniques for consistency with their specifications, even if they employ exception propagation and handling to achieve required results (i.e., nonerror situations). Example verifications are given.

The formal specification, design, implementation, and verification of a compiler for a Pascal-like language is described. All components of the compilation process such as scanning, parsing, type checking, and code generation are considered. The implemented language contains most control structures of Pascal, recursive procedures and functions, and jumps. It provides user defined data types including arrays, records, and pointers. A simple facility for input-output is provided. The target language assumes a stack machine including a display mechanism to handle procedure and function calls. The compiler itself is written in Pascal Plus, a dialect of Pascal accepted by the Stanford verifier. The Stanford verifier is used to give a complete formal machine checked verification of the compiler. One of the main problem areas considered is the formal mathematical treatment of programming languages and compilers suitable as input for automated program verification systems. Several technical and methodological problems of mechanically verifying large software systems are considered. Some new verification techniques are developed, notably methods to reason about pointers, fixed points, and quantification. These techniques are of general importance and are not limited to compiler verification. The result of this research demonstrates that construction of large correct programs is possible with the existing verification technology. It indicates that verification will become a useful software engineering tool in the future. Several problem areas of current verification systems are pointed out and areas for future research are outlined.

We present a method of formal specification of Ada programs containing packages. The method suggests concepts and guidelines useful for giving adequate informal documentation of packages by means of comments.The method depends on (1) the standard inductive assertion technique for subprograms, (2) the use of history sequences in assertions specifying the declaration and use of packages, and (3) the addition of three categories of specifications to Ada package declarations: (a) visible specifications, (b) boundary specifications, (c) internal specifications.Axioms and proof rules for the Ada package constructs (declaration, instantiation, and function and procedure call) are given in terms of history sequences and package specifications. These enable us to construct formal proofs of the correctness of Ada programs with packages. The axioms and proof rules are easy to implement in automated program checking systems. The use of history sequences in both in formal documentation and formal specifications and proofs is illustrated by examples.

A theory of partial correctness proofs is formulated in Scott's logic computable junctions. This theory allows mechanical construction of verification condition solely on the basis of a denotational language definition. Extensionally these conditions, the resulting proofs, and the required program augmentation are similar to those of Hoare style proofs; conventional input, output, and invariant assertions in a first order assertion language are required. The theory applies to almost any sequential language defined by a continuation semantics; for example, there are no restrictions on aliasing or side-effects. Aspects of "static semantics",such as type and declaration constraints, which are expressed in the denotational definition are validated as part of the verification condition generation process.

We develop a formal model describing the basic objects and operations of the software development process. This model allows us to characterize functions performed by support environments and to formally define the semantics of environment tools. Representing information about available tools, administrative procedures, and constraints in a knowledge base allows automated support for many software development and life-cycle activities. Constraint maintenance within a knowledge base takes over many routine administrative tasks; program synthesis techniques can be used to generate complex plans.

Problems and shortcomings of the current maintenance paradigm and the approach to software reuse are analyzed. We argue that knowledge-based transformation techniques will provide solutions in both areas. Such techniques will enable maintenance to be performed on the specification level. Efficient code can be regenerated from changed specifications by replaying recorded design decisions. Program transformations can be used capture and represent general as well as application specific programming knowledge. Reuse of such knowledge is the most flexible and general form of reuse.

In this position paper we discuss the model of software development adopted by Kestrel Institute, how iteration relates to this model, what knowledge-based tools have been developed that support iteration and specific, ongoing research on automating formal program developments.

A formal model for describing the semantics of operations in software engineering environments is presented. The proposed model consists of two parts, a description of the data domains, and an axiomatic definition of tool invocations and their composition. Objects in environments are characterized by their hierarchical composition and by dependencies between their sub-components. A general data model is developed, allowing uniform description of such diverse domains as source programs, requirements, and documentation. A first-order assertion language is introduced. The semantics of tools are described with pre and post conditions in this assertion language. Further, environment goals, such as “release a system x for a target y with property z” can be stated formally. An agenda is a partially ordered set of tool invocations and user actions. A language for describing agendas is defined. A formal semantics for this language is given by set of axiomatic proof rules. Program synthesis and planning techniques can be used to generate an optimal agenda such that its precondition is satisfied in the current state and its post condition implies a given goal statement. Combined with a knowledge base this mechanism can serve as the basis for the development of sophisticated environments that provide automated support for many software development and life-cycle activities.

The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. It scales up properly, in the sense that one can demonstrate the soundness of decomposing an implementation hierarchically and reasoning locally about the implementation of each node in the hierarchy.

The Common Intermediate Design Language (CIDL) is a high-level executable system design language intended for the evolutionary prototyping of large distributed software systems. CIDL was designed to be the target language for code synthesis from high-level system descriptions and the source language for translation in to Ada. The resulting design is a typed language with higher-order functions, polymorphism, and concurrency constructs. The language uses types as a representation of formal specifications.

Modular verification of Ada library units enables programmers to write and verify small program units and to compose them with minimal additional effort into larger correct programs. Penelope is a prototype verification environment for Ada that supports separate verification of program units and their composition. The authors have extended Penelope to enable verification of larger Ada programs, consisting of multiple compilation units. They discuss two major issues that arise from the composition of program modules. The first is ensuring that the composition itself is correct, that is, that assumptions made by one module about another indeed hold. The elaboration of Ada packages poses new problems, which are described along with the solution adopted. A novel technique for reducing the amount of annotation required from the user is described. The second issue is maintaining consistency between the various modules without incurring excessive overhead. The way in which a set of modules is kept consistent depends on the structure of the language. The method, called separate verification, is closely modeled on the technique of separate compilation used in Ada. How Ada techniques can be adapted for a verification environment is discussed

Richard Feynman's observation that quantum mechanical effects could not be simulated efficiently on a computer led to speculation that computation in general could be done more efficiently if it used quantum effects. This speculation appeared justified when Peter Shor described a polynomial time quantum algorithm for factoring integers. In quantum systems, the computational space increases exponentially with the size of the system which enables exponential parallelism. This parallelism could lead to exponentially faster quantum algorithms than possible classically. The catch is that accessing the results, which requires measurement, proves tricky and requires new non-traditional programming techniques. The aim of this paper is to guide computer scientists and other non-physicists through the conceptual and notational barriers that separate quantum computing from conventional computing. We introduce basic principles of quantum mechanics to explain where the power of quantum computers comes from and why it is difficult to harness. We describe quantum cryptography, teleportation, and dense coding. Various approaches to harnessing the power of quantum parallelism are explained, including Shor's algorithm, Grover's algorithm, and Hogg's algorithms. We conclude with a discussion of quantum error correction.

We present efficient implementations of a number of operations for quantum computers. These include controlled phase adjustments of the amplitudes in a superposition, permutations, approximations of transformations and generalizations of the phase adjustments to block matrix transformations. These operations generalize those used in proposed quantum search algorithms.

Richard Feynman's observation that quantum mechanical effects could not be simulated efficiently on a computer led to speculation that computation in general could be done more efficiently if it used quantum effects. This speculation appeared justified when Peter Shor described a polynomial time quantum algorithm for factoring integers. In quantum systems, the computational space increases exponentially with the size of the system which enables exponential parallelism. This parallelism could lead to exponentially faster quantum algorithms than possible classically. The catch is that accessing the results, which requires measurement, proves tricky and requires new non-traditional programming techniques. The aim of this paper is to guide computer scientists and other non-physicists through the conceptual and notational barriers that separate quantum computing from conventional computing. We introduce basic principles of quantum mechanics to explain where the power of quantum computers comes from and why it is difficult to harness. We describe quantum cryptography, teleportation, and dense coding. Various approaches to harnessing the power of quantum parallelism are explained, including Shor's algorithm, Grover's algorithm, and Hogg's algorithms. We conclude with a discussion of quantum error correction.

We describe a genetic segmentation algorithm for image data streams and video. This algorithm operates on segments of a string representation. It is similar to both classical genetic algorithms that operate on bits of a string and genetic grouping algorithms that operate on subsets of a set. It employs a segment fair crossover operation. For evaluating segmentations, we define similarity adjacency functions, which are extremely expensive to optimize with traditional methods. The evolutionary nature of genetic algorithms offers a further advantage by enabling incremental segmentation. Applications include browsing and summarizing video and collections of visually rich documents, plus a way of adapting to user access patterns.

We describe a genetic segmentation algorithm for video. This algorithm operates on segments of a string representation. It is similar to both classical genetic algorithms that operate on bits of a string and genetic grouping algorithms that operate on subsets of a set. For evaluating segmentations, we define similarity adjacency functions, which are extremely expensive to optimize with traditional methods. The evolutionary nature of genetic algorithms offers a further advantage by enabling incremental segmentation. Applications include video summarization and indexing for browsing, plus adapting to user access patterns.

A dependency action system uses redundant sets of dynamically reconfigurable functional components to achieve robustness and fault tolerance, and to achieve self-optimization by learning and planning techniques that use time-stamps and or computation stamps as a key indicator. The dependency action system is based on functional components, or actions, which act on data values that are stored in stamped storage locations. Data is read and written to these storage locations, updating the stamps as appropriate. The execution of an action is controlled by the stamps of its enabling and disabling storage locations. The dependency action system specifies an action as enabled if new data has arrived in the enabling storage locations. Updating the stamp of the disabling storage locations disables the action. If an alternative action succeeds and produces a value, the other alternative actions become disabled. If one action fails to produce a value to a storage location, other alternative actions may still be enabled and can be executed. Thus, the dependency action system supports automatic recovery from failure of an individual action. The dependency action system accumulates statistical information about the behavior of the actions, which includes the probability that a particular disabling storage location will be updated by an action and the average cost of an action. The dependency action system uses this information to plan a sequence of action executions that most likely leads to the cheapest solution of a given task.

Technology transfer from academic research to industrial practice is hampered by social, political, and economic problems more than by technical issues. This paper describes one instance of successful technology transfer based on a special-purpose language and an associated translation tool tailored to the customer's needs. The key lesson to be learned from this example is that mathematical formalisms must be transparent to the user. Formalisms can be effectively employed if they are represented by tools that fit into existing work processes. It is suggested that special-purpose, domain-specific languages and their translators are an important vehicle to transition advanced technology to practice. This approach enables domain experts to solve problems using familiar terminology. It enables engineers of all disciplines to utilize computers without becoming software engineers. In doing so, we not only mitigate the chronic shortage of qualified software personnel but also simplify the problem of requirements analysis and specification.

New technologies are constructed from technologies that previously exist, and in turn these new technologies offer themselves as possible components---building blocks---for the construction of further new technologies. Thus in 1912 the amplifier circuit was constructed from the already existing triode vacuum tube in combination with other circuit components. It in turn made possible the oscillator and the heterodyne mixer; which together with other standard components made possible continuous-wave radio transmission. The collective of technology in this way forms a network of elements where novel elements are created from existing ones and where more complicated elements evolve from simpler ones. We model this phenomenon of technology creating itself by setting up an artificial system in which new elements (logic circuits) build themselves from simpler existing elements, and we study the properties of the resulting build-out.

A method, information system, and computer-readable medium is provided for segmenting a plurality of data, such as multimedia data, and in particular an image document stream. Segment boundary points may be used for retrieving and/or browsing the plurality of data. Similarly, segment boundary points may be used to summarize the plurality of data. Examples of image document streams include video, PowerPoint slides, and NoteLook pages. A genetic method having a fitness or evaluation function using information retrieval concepts, such as importance and precedence, is used to obtain segment boundary points. The genetic method is able to evaluate a large amount of data in a cost effective manner. The genetic method is also able to run incrementally on streaming video and adapt to usage patterns by considering frequently accessed images.

The MediaMetro application provides an interactive 3D visualization of multimedia document collections using a city metaphor. The directories are mapped to city layouts using algorithms similar to treemaps. Each multimedia document is represented by a building and visual summaries of the different constituent media types are rendered onto the sides of the building. From videos, Manga storyboards with keyframe images are created and shown on the façade; from slides and text, thumbnail images are produced and subsampled for display on the building sides. The images resemble windows on a building and can be selected for media playback. To support more facile navigation between high overviews and low detail views, a novel swooping technique was developed that combines altitude and tilt changes with zeroing in on a target.

Technology -- the collection of devices and methods available to human society -- evolves by constructing new devices and methods from ones that previously exist, and in turn offering these as possible components -- building blocks -- for the construction of further new devices and elements. The collective of technology in this way forms a network of elements where novel elements are created from existing ones and where more complicated elements evolve from simpler ones. We model this evolution within a simple artificial system on the computer. The elements in our system are logic circuits. New elements are formed by combination from simpler existing elements (circuits), and if a novel combination satisfies one of a set of needs, it is retained as a building block for further combination. We study the properties of the resulting build out. We find that our artificial system can create complicated technologies (circuits), but only by first creating simpler ones as building blocks. Our results mirror Lenski et al.'s: that complex features can be created in biological evolution only if simpler functions are first favored and act as stepping stones. We also find evidence that the resulting collection of technologies exists at self-organized criticality.

During grouping tasks for data exploration and sense-making, the criteria are normally not well-defined. When users are bringing together data objects thought to be similar in some way, implicit brushing continually detects for groups on the freeform workspace, analyzes the groups2̆019 text content or metadata, and draws attention to related data by displaying visual hints and animation. This provides helpful tips for further grouping, group meaning refinement and structure discovery. The sense-making process is further enhanced by retrieving relevant information from a database or network during the brushing. Closely related to implicit brushing, target snapping provides a useful means to move a data object to one of its related groups on a large display. Natural dynamics and smooth animations also help to prevent distractions and allow users to concentrate on the grouping and thinking tasks. Two different prototype applications, note grouping for brainstorming and photo browsing, demonstrate the general applicability of the technique.

Load balancing has been an increasingly important issue for handling computational intensive tasks in a distributed system such as in Grid and cluster computing. In such systems, multiple server instances are installed for handling requests from client applications, and each request (or task) typically needs to stay in a queue before an available server is assigned to process it. In this paper, we propose a high-performance queueing method for implementing a shared queue for collaborative clusters of servers. Each cluster of servers maintains a local queue and queues of different clusters are networked to form a unified (or shared) queue that may dispatch tasks to all available servers. We propose a new randomized algorithm for forwarding requests in an overcrowded local queue to a networked queue based on load information of the local and neighboring clusters. The algorithm achieves both load balancing and locality awareness.

A provably correct computer program can be generated using genetic programming techniques. A desired behavior is used to define a formal specification. An initial population of programs is created where each program has a meaning that can be defined using a formalization technique. A fitness function is applied to measure a distance between the meaning of a program, i.e., its actual behavior, and the specification. Any program having a zero value as the measure of distance between the meaning of the program and the specification is determined to be provably correct. After the fitness of some or all of the programs in the current generation of programs has been computed, a provably correct program has not yet been found in the current generation, mutation and/or crossover techniques are performed on at least some of the fittest individuals in the current generation to create the programs of a next generation.

Wireless networking is becoming widespread in many public places such as cafes. Unsuspecting users may become victims of attacks based on “evil twin” access points. These rogue access points are operated by criminals in an attempt to launch man-in-the-middle attacks. We present a simple protection mechanism against binding to an evil twin. The mechanism leverages short authentication string protocols for the exchange of cryptographic keys. The short string verification is performed by encoding the short strings as a sequence of colors, rendered sequentially by the user's device and by the designated access point of the cafe. The access point must have a light capable of showing two colors and must be mounted prominently in a position where users can have confidence in its authenticity. We conducted a usability study with patrons in several cafes and participants found our protection mechanism very usable.

In this video demo, we present mTable, a multimedia tabletop system for browsing photo and video collections. We have developed a set of applications for visualizing and exploring photos, a board game for labeling photos, and a 3D cityscape metaphor for browsing videos. The system is suitable for use in a living room or office lounge, and can support multiple displays by visualizing the collections on the tabletop and showing full-size images and videos on another flat panel display in the room.

The present invention relates to a method to make effective use of non rectangular display space for displaying a collage. In an embodiment of the invention, a heterogeneous set of images can be arranged to display the region of interest of the images to avoid overlapping regions of interest. The background gaps between the regions of interest can be filled by extending the regions of interest using a Voronoi technique. This produces a stained class effect for the collage. In an embodiment of the present invention, the technique can be applied to irregular shapes including circular shapes with a hole in the middle. In an embodiment of the present invention, the technique can be used to print labels for disks.