Computer Sciences Colloquium - EFFICIENTLY REASONING ABOUT PROGRAMS

Neil Immerman - Lecturer, Mortimer & Raymond Sackler Institute of Advanced Studies

21 May 2017, 11:00 
Schreiber Building, Room 006 
Computer Sciences Colloquium

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.

Tel Aviv University, P.O. Box 39040, Tel Aviv 6997801, Israel
Developed by
UI/UX Basch_Interactive