DECISION PROCEDURES FOR VERIFICATION   . . . Abstract . . . Biography Harvey Friedman, Ohio State University     4:00 PM (refreshments 3:45), Stata Center, 32G-7th Floor Lounge CSAIL Seminar -   Host: Vijay Ganesh, MIT-CSAIL -   Contact: Mary McDavitt, mmcdavit@csail.mit.edu

Abstract

We discuss some decision procedures involving finite strings, and explore the boundary between decidability and undecidability. A form of some of these decision procedures has been implemented and is being used to automatically verify VCs (verification conditions) arising from various basic string processing programs written in an imperative language (the language RESOLVE developed at Ohio State). We also discuss some decidability and undecidability issues surrounding the basic JAVA operation of string replacement.