polak.bib

@inproceedings{Pol76-1,
  author = {W. Polak},
  title = {Anwendung der axiomatischen {D}efinitionsmethode auf h\"{o}here {P}rogrammierspra\-chen},
  booktitle = {Programmiersprachen, 4. Fachtagung der GI},
  pages = {12--18},
  year = {1976},
  editor = {H.-J. Schneider and M. Nagl},
  volume = {1},
  series = {Informatik-Fachberichte},
  address = {Berlin},
  month = mar,
  publisher = {Springer Verlag},
  url = {http://portal.acm.org/citation.cfm?id=646610.696645}
}
@article{Pol79-1,
  author = {Wolfgang Polak},
  month = sep,
  year = {1979},
  title = {An exercise in automatic program verification},
  journal = {IEEE Transactions of Software Engineering},
  volume = {SE--5},
  number = {5},
  pages = {453--458},
  abstract = {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.},
  url = {http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?isnumber=35912&arnumber=1702654&count=17&index=3}
}
@techreport{LGHKMOPS79-2,
  author = {David C. Luckham and Steven M. German and Friedrich W. von Henke
             and Richard A. Karp and P. W. Milne and Derek C. Oppen and
             Wolfgang Polak and William L. Scherlis},
  title = {Stanford Pascal Verifier user manual},
  institution = {Stanford University, Department of Computer Science},
  type = {Technical Report},
  number = {STAN-CS-TR-79-731},
  pages = {124},
  month = mar,
  year = {1979},
  abstract = {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.}
}
@techreport{LP80-1,
  author = {David C. Luckham and Wolfgang Polak},
  title = {{Ada} exceptions: specification and proof techniques},
  institution = {Stanford University, Department of Computer Science},
  type = {Technical Report},
  number = {STAN-CS-TR-80-789},
  pages = {20},
  month = feb,
  year = {1980},
  url = {http://www.pocs.com/Papers/CS-TR-80-789.pdf},
  abstract = {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.}
}
@article{LP80-2,
  author = {David C. Luckham and W. Polak},
  title = {{Ada} exception handling: an axiomatic approach},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {2},
  number = {2},
  pages = {225--233},
  month = apr,
  year = {1980},
  issn = {0164-0925},
  url = {http://doi.acm.org/10.1145/357094.357100},
  abstract = {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.}
}
@techreport{Pol80-3,
  author = {Wolfgang Heinz Polak},
  month = may,
  year = {1980},
  title = {Theory of compiler specification and verification},
  number = {STAN-CS-80-802},
  institution = {Stanford University},
  address = {Stanford, CA},
  abstract = {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.}
}
@article{LP80-4,
  author = {David C. Luckham and Wolfgang Polak},
  title = {A Practical Method of Documenting and Verifying {Ada} Programs with
           Packages},
  journal = {1980 SIGPlan Symposiun on the {Ada} Programing Language},
  pages = {113--122},
  publisher = {ACM SIGPlan},
  address = {New York, NY},
  month = dec,
  year = {1980},
  url = {http://doi.acm.org/10.1145/948632.948648},
  abstract = {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.}
}
@inproceedings{Pol81-1,
  key = {Polak},
  author = {Wolfgang Polak},
  title = {Program Verification Based on Denotational Semantics},
  booktitle = {Conference Record of the Eighth ACM Symposium on Principles of
           Programming Languages},
  publisher = {ACM},
  month = jan,
  year = {1981},
  pages = {149--158},
  annote = {24 references.},
  url = {http://www.pocs.com/Papers/POPL-81.pdf},
  abstract = {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.}
}
@inproceedings{Pol81-2,
  author = {W. Polak},
  title = {Program Verification at Stanford - Past, Present, Future},
  booktitle = {Workshop on Artificial Intelligence},
  pages = {256--276},
  year = {1981},
  editor = {J. Siekman},
  volume = {47},
  series = {Informatik-Fachberichte},
  address = {Berlin},
  publisher = {Springer Verlag},
  url = {http://portal.acm.org/citation.cfm?id=647602.732391}
}
@book{Pol81-3,
  author = {W. Polak},
  title = {Compiler Specification and Verification},
  publisher = {Springer},
  address = {Berlin},
  year = {1981},
  isbn = {3-540-10886-6},
  volume = {124},
  series = {Lecture Notes in Computer Science},
  url = {http://www.amazon.com/gp/product/0387108866/104-5132917-1174311?n=283155}
}
@inproceedings{Pol86-1,
  author = {Wolfgang Polak},
  title = {Framework for a Knowledge-Based Programming Environment},
  booktitle = {Int'l Workshop on Programming Environments},
  year = {1986},
  volume = {244},
  series = {Lecture Notes in Computer Science},
  address = {Trondheim, Norway},
  month = jun,
  pages = {566--574},
  publisher = {Springer Verlag},
  abstract = {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.}
}
@unpublished{Pol86-2,
  author = {Wolfgang Polak},
  title = {{AI} Approaches to Software Engineering},
  note = {Workshop on Complementary Approaches to Software Engineering, Imperial College, London},
  month = jun,
  year = {1986}
}
@inproceedings{Pol86-3,
  author = {Wolfgang Polak},
  title = {Maintainability and Reusable Program Designs},
  booktitle = {Conf.~on Software Reusability and Maintainability},
  year = {1986},
  address = {Tysons Corner, VA},
  month = sep,
  abstract = {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.}
}
@inproceedings{GCPJ86-4,
  author = {Allen Goldberg and Cordell Green and Wolfgang Polak and Richard
           Juellig},
  title = {Iteration in the software process},
  booktitle = {Proceedings of the ~$3^{rd}$~ International Software Process
           Workshop},
  year = {1986},
  editor = {M. Dowson},
  pages = {105--108},
  month = nov,
  abstract = {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.},
  url = {http://www.amazon.com/Iteration-Software-Process-Proceedings-International/dp/0818607092/ref=sr_1_126/104-6783173-7179944?ie=UTF8&s=books&qid=1176587271&sr=1-126}
}
@techreport{Pol87-1,
  author = {Wolfgang Polak},
  title = {Framework for a Knowledge-Based Programming Environment},
  institution = {Kestrel Institute},
  year = {1987},
  number = {KES.U.86.3},
  month = jun,
  abstract = {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.}
}
@techreport{JLGP87-2,
  author = {Richard Jullig and Peter Ladkin and Li-Mei Gilham and Wolfgang Polak},
  title = {{KBSA} Project Management Assistant Final Technical Report (2 vols)},
  institution = {Rome Air Development Center},
  year = {1987},
  number = {RADC-TR-87-78},
  month = jul
}
@misc{JPLG87-3,
  author = {R. Jullig and W. Polak and P. Ladkin and L. Gilham},
  title = {Knowledge-Based Software Project Management},
  howpublished = {Technical Report KES.U.87.3, Kestrel Institute},
  year = {1987}
}
@misc{Pol88-1,
  author = {W. Polak},
  title = {A Technique for Defining Predicate Transformers},
  howpublished = {Technical Report 17-4, Odyssey Research Associates, Ithaca, NY, October},
  year = {1988}
}
@misc{Pol89-1,
  author = {W. Polak},
  title = {Predicate transformer semantics for {Ada}},
  howpublished = {Technical Report 89-39, Odyssey Research Associates, September},
  year = {1989}
}
@article{GMP90-1,
  author = {David Guaspari and Carla Marceau and Wolfgang Polak},
  title = {Formal Verification of {Ada} Programs},
  journal = {IEEE Transactions on Software Engineering},
  volume = {16},
  number = {9},
  month = sep,
  year = {1990},
  pages = {1058--1075},
  annote = {Penelope verification editor and Larch/Ada. 35 references.},
  url = {http://csdl.computer.org/comp/trans/ts/1990/09/e1058abs.htm},
  abstract = {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.}
}
@misc{GP91,
  author = {H. Graves and W. Polak},
  title = {Common Intermediate Design Language Overview},
  howpublished = {Lockheed Palo Alto Research Laboratory},
  year = {1991}
}
@incollection{GMP92-1,
  author = {David Guaspari and Carla Marceau and Wolfgang Polak},
  title = {Formal Verification of {Ada} Programs},
  editor = {Ursala Martin and Jeanete M. Wing},
  booktitle = {First International Workshop on Larch, Dedham 1992},
  publisher = {Springer-Verlag},
  year = {1992},
  pages = {104--141},
  annote = {35 references}
}
@inproceedings{GP92-2,
  author = {W.H. Graves and W. Polak},
  title = {Common Intermediate Design Language},
  booktitle = {Hawaii International Conference on System Sciences},
  year = {1992},
  month = jan,
  url = {http://ieeexplore.ieee.org/iel2/378/4717/00183264.pdf?isnumber=&arnumber=183264},
  abstract = {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.}
}
@inproceedings{MP92-3,
  author = {Carla Marceau and Wolfgang Polak},
  title = {Modular Verification of {Ada} Library Units},
  booktitle = {Seventh Annual Conference on Computer Assurance},
  year = {1992},
  address = {Gaithersburg},
  month = jun,
  url = {http://ieeexplore.ieee.org/iel2/636/6057/00235764.pdf?isnumber=&arnumber=235764},
  abstract = {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}
}
@misc{GMPS95-1,
  author = {David Guaspari and John McHugh and Wolfgang Polak and Mark Saaltink},
  title = {Towards a Formal Semantics for {Ada} {9X}},
  howpublished = {NASA Contractor Report 195037},
  month = mar,
  year = {1995},
  url = {http://www.pocs.com/Papers/Ada-oct94.pdf}
}
@inproceedings{PNB95-2,
  author = {Wolfgang Polak and Lester D. Nelson and Timothy W. Bickmore},
  title = {Reengineering {IMS} Databases to Relational Systems},
  booktitle = {7th annual Software Technology Conference},
  year = {1995},
  address = {Salt Lake City},
  month = apr,
  note = {published on CDROM}
}
@techreport{RP98-1,
  author = {Eleanor Rieffel and Wolfgang Polak},
  title = {Introduction to Quantum Computing for Non-Physicists},
  institution = {FX Palo Alto Laboratory},
  year = {1998},
  number = {TR-98-044},
  month = aug,
  abstract = {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.},
  url = {http://xxx.lanl.gov/abs/quant-ph/9809016}
}
@inproceedings{Pol98-2,
  author = {Wolfgang Polak},
  title = {Formal Methods in Practice},
  booktitle = {Proceedings of The 1998 ARO/\-ONR/\-NSF/\-DARPA Monterey Workshop on Engineering Automation for Computer Based Systems},
  year = {1998},
  number = {NPS-CS-99-00},
  address = {Monterey, California},
  series = {Naval Postgraduate School}
}
@article{HMPR99-1,
  author = {Tad Hogg and Carlos Mochon and Wolfgang Polak and Eleanor Rieffel},
  title = {Tools for Quantum Algorithms},
  journal = {International Journal of Modern Physics C},
  year = {1999},
  volume = {10},
  number = {7},
  pages = {1347-1361},
  url = {http://arxiv.org/abs/quant-ph/9811073},
  abstract = {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.}
}
@article{RP00-1,
  author = {Eleanor Rieffel and Wolfgang Polak},
  title = {An Introduction to Quantum Computing for Non-Physicists},
  journal = {ACM Computing Surveys},
  year = {2000},
  number = {3},
  volume = {32},
  month = sep,
  pages = {300--335},
  url = {http://doi.acm.org/10.1145/367701.367709},
  abstract = {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.}
}
@article{RP00-2,
  author = {Eleanor Rieffel and Wolfgang Polak},
  title = {Introduction to Quantum Computing (in {R}ussian)},
  journal = {Quantum Computers and Computing},
  year = {2000},
  number = {1},
  volume = {1},
  pages = {4--57},
  note = {R\&C Dynamics, Moscow},
  url = {http://www.pocs.com/qc/qc-tut-ru.pdf}
}
@inproceedings{PGPRWB00-3,
  author = {Patrick Chiu and Andreas Girgensohn and Wolfgang Polak and Eleanor Rieffel and Lynn Wilcox and Forrest H. Bennett III},
  title = {A Genetic Segmentation Algorithm for Image Data Streams and Video},
  booktitle = {Genetic and Evolutionary Computation Conference},
  year = {2000},
  address = {Las Vegas, NV},
  url = {http://www.pocs.com/Papers/FXPAL-PR-00-115.pdf},
  abstract = {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. }
}
@inproceedings{PGPRW00-4,
  author = {Patrick Chiu and Andreas Girgensohn and Wolfgang Polak and Eleanor Rieffel and Lynn Wilcox},
  title = {A Genetic Algorithm for Video Segmentation and Summarization},
  booktitle = {IEEE International Conference on Multimedia and Expo},
  year = {2000},
  address = {New York, NY},
  organization = {IEEE},
  url = {http://www.pocs.com/Papers/FXPAL-PR-00-114.pdf},
  abstract = {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.}
}
@manual{PoPat01-1,
  title = {Method and System for Constructing Adaptive and Resilient Software.},
  author = {Wolfgang Polak},
  organization = {US Patent 6,226,627 B1},
  month = {May},
  year = 2001,
  abstract = {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.},
  url = {http://patft.uspto.gov/netacgi/nph-Parser?Sect1=PTO1&Sect2=HITOFF&d=PALL&p=1&u=/netahtml/srchnum.htm&r=1&f=G&l=50&s1=6,226,627.WKU.&OS=PN/6,226,627&RS=PN/6,226,627}
}
@article{SCP02-1,
  author = {Wolfgang Polak},
  title = {Formal Methods in Practice},
  journal = {Science of Computer Programming},
  year = 2002,
  volume = 42,
  number = 1,
  pages = {75-85},
  month = {Jan},
  abstract = {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. }
}
@techreport{AP04-1,
  author = {Brian Arthur and Wolfgang Polak},
  title = {The Evolution of Technology within a Simple Computer Model},
  institution = {Santa Fe Institute},
  year = {2004},
  number = {},
  month = dec,
  url = {http://www.pocs.com/Papers/SFI-04-12-042.pdf},
  abstract = {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.}
}
@manual{CGLPSP04-2,
  title = {Systems and methods for creating an interactive 3d visualization of indexed media},
  author = {Patrick Chiu and Andreas Girgensohn and Surapong Lertsithichai and Wolfgang Polak and Frank Shipman},
  organization = {US Patent, US 20080104546 A1},
  year = 2008
}
@manual{CGPRWBP04-3,
  title = {A genetic algorithm for summarizing image document streams and video key frame selection},
  author = {Patrick Chiu and Andreas Girgensohn and Wolfgang Polak and Eleanor Rieffel and Lynn Wilcox and Forrest Bennett},
  organization = {US Patent 6,819,795},
  month = nov,
  year = 2004,
  abstract = {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.},
  url = {http://patft.uspto.gov/netacgi/nph-Parser?Sect1=PTO1&Sect2=HITOFF&d=PALL&p=1&u=%2Fnetahtml%2FPTO%2Fsrchnum.htm&r=1&f=G&l=50&s1=6,819,795.PN.&OS=PN/6,819,795&RS=PN/6,819,795}
}
@inproceedings{CGLPS05-1,
  author = {Patrick Chiu and Andreas Girgensohn and Surapong Lertsithichai and Wolfgang Polak and Frank Shipman},
  title = {MediaMetro: Browsing Multimedia Document Collections with a 3D City Metaphor},
  booktitle = {ACM Multimedia 2005, Technical Demonstrations},
  year = {2006},
  month = nov,
  url = {http://www.pocs.com/Papers/FXPAL-PR-05-334.pdf},
  abstract = {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. }
}
@manual{PAPat05-2,
  title = {System and Method for Automatic Design of Components in Libraries},
  author = {Wolfgang Polak and W.~Brian Arthur},
  organization = {US Patent 7,711,674 B2},
  month = may,
  year = 2007
}
@article{AP06-1,
  author = {W.~Brian Arthur and Wolfgang Polak},
  title = {The Evolution of Technology within a Simple Computer Model},
  journal = {Complexity},
  publisher = {Wiley},
  year = {2006},
  volume = 11,
  number = 5,
  pages = {23-31},
  month = {May},
  url = {http://dx.doi.org/10.1002/cplx.v11:5},
  abstract = {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. }
}
@inproceedings{SCHBP06-2,
  author = {Xiaohua Sun and Patrick Chiu and Jeffrey Huang and Maribeth Back and Wolfgang Polak},
  title = {Implicit Brushing and Target Snapping: Data Exploration and Sense-making on Large Displays},
  booktitle = {Proceedings of AVI},
  year = {2006},
  month = may,
  publisher = {ACM Press},
  url = {http://www.pocs.com/Papers/FXPAL-PR-06-368.pdf},
  abstract = {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 groups\u2019 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.}
}
@inproceedings{LP06-3,
  author = {Cheng-Jia Lai and Wolfgang Polak},
  title = {A Collaborative Approach to Stochastic Load Balancing with Networked Queues of Autonomous Service Clusters},
  booktitle = {MobCops 2006 Workshop},
  year = {2006},
  organization = {IEEE/ACM},
  address = {Atlanta, Georgia},
  month = nov,
  abstract = {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. },
  url = {http://www.fxpal.com/publications/FXPAL-PR-06-384.pdf}
}
@manual{PoPat07-1,
  title = {A Method for Automatically Generating Provably Correct Code},
  author = {Wolfgang Polak},
  organization = {US Patent, 7,243,086},
  year = 2007,
  abstract = {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.},
  url = {http://patft.uspto.gov/netacgi/nph-Parser?Sect1=PTO1&Sect2=HITOFF&d=PALL&p=1&u=%2Fnetahtml%2FPTO%2Fsrchnum.htm&r=1&f=G&l=50&s1=7243086.PN.&OS=PN/7243086&RS=PN/7243086}
}
@inproceedings{RPRT08-1,
  author = {Volker Roth and Wolfgang Polak and Eleanor Rieffel and Thea Turner},
  title = {Simple and Effective Defense Against Evil Twin Access Points},
  booktitle = {WiSec '08: Proceedings of the first ACM conference on Wireless network security},
  pages = {220-235},
  year = {2008},
  isbn = {978-1-59593-814-5},
  location = {Alexandria, VA, USA},
  publisher = {ACM},
  address = {New York, NY, USA},
  abstract = {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. },
  url = {http://www.fxpal.com/publications/FXPAL-PR-08-428.pdf}
}
@inproceedings{CHBDDPS2008,
  title = {mTable: browsing photos and videos on a tabletop
		 system},
  author = {Patrick Chiu and Jeffrey Huang and Maribeth Back and
		 Nicholas Diakopoulos and John Doherty and Wolfgang
		 Polak and Xiaohua Sun},
  bibdate = {2008-11-24},
  bibsource = {DBLP,
		 http://dblp.uni-trier.de/db/conf/mm/mm2008.html#ChiuHBDDPS08},
  booktitle = {Proceedings of the 16th International Conference on
		 Multimedia 2008, Vancouver, British Columbia, Canada,
		 October 26-31, 2008},
  publisher = {ACM},
  year = {2008},
  editor = {Abdulmotaleb El-Saddik and Son Vuong and Carsten
		 Griwodz and Alberto Del Bimbo and K. Sel{\c c}uk Candan
		 and Alejandro Jaimes},
  isbn = {978-1-60558-303-7},
  pages = {1107--1108},
  url = {http://www.youtube.com/watch?v=JdLKvfDRqj0&feature=channel_page},
  abstract = {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.}
}
@book{EP11-1,
  author = {Eleanor Rieffel and Wolfgang Polak},
  title = {Quantum Computing, a Gentle Introduction},
  publisher = {MIT Press},
  address = {Cambridge, MA},
  year = {2011},
  isbn = {0-262-01506-4},
  url = {http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=12555}
}
@manual{PoPat12-1,
  title = {Annealing Algorithm for Non-Rectangular shaped Stained Glass Collages},
  author = {Kazumasa Murai and Patrick Chiu and Wolfgang Polak and Andreas Girgensohn and Qiong Liu},
  organization = {US Patent 8,144,919 B2},
  month = {Mar},
  year = 2012,
  abstract = {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.},
  url = {http://patft.uspto.gov/netacgi/nph-Parser?Sect1=PTO1&Sect2=HITOFF&d=PALL&p=1&u=%2Fnetahtml%2FPTO%2Fsrchnum.htm&r=1&f=G&l=50&s1=8,144,919.PN.&OS=PN/8,144,919&RS=PN/8,144,919}
}
@manual{PoPat13-1,
  title = {System and Method for Human Assisted Secure Information Exchange},
  author = {Volker Roth and Wolfgang Polak and Eleanor Rieffel},
  organization = {US Patent 8,429,405 B2},
  month = {Apr},
  year = 2013
}
@manual{PoPat14-1,
  title = {Biologically based chamber matching},
  author = {Sanjeev Kaushal and Kenji Sugishima and Sukesh Janubhai Patel and Robert Filman and Wolfgang Polak and Orion Wolfe and Jessie Burger},
  organization = {US Patent 8,723,869 B2},
  month = {May},
  year = 2014
}
@manual{PoPat17-1,
  title = {Method and apparatus for autonomous tool parameter impact identification system for semiconductor manufacturing},
  author = {Sanjeev Kaushal and Sukesh Janubhai Patel and Wolfgang Polak and Aaron Archer Waterman and Orion Wolfe},
  organization = {US Patent 9746849},
  month = {August},
  year = 2017
}

This file was generated by bibtex2html 1.98.