Decision Problems In Strings and Formal Methods
University Professor of Mathematics, Philosophy, and Computer Science, Ohio State
We focus on two formal methods contexts which generate
investigations into decision problems for finite strings.
• RESOLVE Verification Conditions (VCs)
• JAVA Pathfinder
At Ohio State and elsewhere, formal specifications are
given and annotated programs are written (providing loop invariants) that are
designed to meet those specifications. This generates mathematical statements
called VCs (verification conditions), which guarantee that the annotated
program meets the specifications.
In the context of finite strings, decision procedures 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 written in RESOLVE.
We also discuss the boundary between the decidable and
Harvey M. Friedman is Distinguished University Professor
of Mathematics, Philosophy, and Computer Science at The Ohio State University
in Columbus, Ohio, USA. He was the recipient of the 1984 Waterman Award given
annually to one researcher covering all fields of science and engineering, for
"his revitalization of the foundations of mathematics, his penetrating
investigations into the Goedel incompleteness phenomena, and his fundamental
contributions to virtually all areas of mathematical logic".
Friedman is best known for his creation of Reverse
Mathematics, whereby logical equivalences between theorems and axioms are
systematically established, and Concrete Mathematical Incompleteness, whereby
Goedel's incompleteness phenomena is systematically extended to various
contexts in Borel measurable, discrete, and finite mathematics. His research
monograph Boolean Relation Theory and Incompleteness will appear in the Lecture
Notes in Logic series of the Association of Symbolic Logic.