Harvey Friedman
Ohio State University
Decision
Problems in Strings and Formal Methods
Abstract:
We focus
on two formal methods contexts which generate investigations into
decision problems for finite strings.
At Ohio State and elsewhere, formal specifications are given and
annotated programs are written (giving pre and post conditions) that
are designed to meet those specifications. This generates mathematical
statements called VCs (verification conditions), which guarantee that
the annotated program meets the specifications. If the context is
finite strings, then decision procedures for finite strings can be very
useful.
We discuss such a decision procedure which we formulated based on our
examination of the VCs generated at Ohio State from string processing
programs. We also discuss the boundary between the decidable and
undecidable.
A second source of decision procedure investigations is suggested by a
tool for JAVA programs called JAVA PATHFINDER. This is a tool to
automatically detect dead code in JAVA programs. It exploits the
structure of JAVA programs, and is based on recognizing the
impossibility of satisfying finitely many conditions. This
naturally leads to a very
wide ranging investigation into decision procedures involving the
primitives in JAVA libraries, such as string replacement x[y/z]. We
discuss some
decidability and undecidability results.
This is a joint Algorithms/POP seminar
Appointments: Nicole Stenger <nstenger@cs.cmu.edu>
Friday, March
27, 2009
3:30 p.m.
Wean
Hall 4623
Principles
of Programming Seminars