Harvey Friedman
Ohio State University

Decision Problems in Strings and Formal Methods

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