Harvard Theory of Computation Seminar

Decision Procedures for Verification

Harvey M. Friedman, Ohio State University

October 9, 2009, Pierce Hall 100F at 3:00PM

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).