DECISION PROCEDURES FOR VERIFICATION
Speaker: Harvey Friedman, Ohio State University
Date: Wednesday, November 4 2009
Time: 5:00PM to 6:00PM
Refreshments: 4:45PM
Location: 32G-7th Floor Lounge
Host: Vijay Ganesh, MIT-CSAIL
Contact: Mary McDavitt, mmcdavit@csail.mit.edu
Relevant URL: 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.
Brief Bio:
Harvey Friedman is one of the leading mathematical logician of our time,
currently a professor at Ohio State University in Columbus, Ohio. He is noted
especially for his work on reverse mathematics, a project intended to derive
the axioms of mathematics from the theorems considered to be necessary. In
recent years this has advanced to a study of Boolean relation theory, which
attempts to justify large cardinal axioms by demonstrating their necessity for
deriving certain propositions considered "concrete".
Friedman earned his Ph.D. from the Massachusetts Institute of Technology in
1967, with a dissertation on Subsystems of Analysis. His advisor was Gerald
Sacks. Friedman received the Alan T. Waterman Award in 1984. He delivered the
Tarski lectures in 2007.
See other events happening in November 2009
