קולוקוויום בביה"ס למדעי המחשב - EFFICIENTLY REASONING ABOUT PROGRAMS

Abstract

When Alan Turing defined his computing machines in his original 1936 paper, he proved that even the simplest problems about their behavior, e.g., does a given machine when started on input 0 eventually halt, was not computable.  Thirty-five years later, Steve Cook presented SAT as the first NP-complete problem.  The understanding was that SAT was an inherently infeasible computational problem.  Now that a large and increasing part of our world is organized and controlled by computer programs, we need as much automatic help as possible to assure that our programs safely and faithfully do what they should do. In this talk, I will describe a language and methodology that has been built up to reason about properties of programs, including the reachability of pointers in programs that destructively update data structures.  We automatically define correctness conditions for these programs.  These are translated to SAT problems and then, in practice, efficiently checked using SAT solvers.