Abstract
Unfortunately, the problem of determining whether a program is correct is undecidable. Program-analysis and verification tools sidestep the tar-pit of undecidability by working on an abstraction of a program, which over-approximates the behavior of the original program. The theory underlying this approach is called abstract interpretation. Abstract interpretation provides a way to obtain information about the possible states that a program reaches during execution, but without actually running the program on specific inputs. Instead, it explores the program's behavior for all possible inputs, thereby accounting for all possible states that the program can reach. Operationally, one can think of abstract interpretation as running the program “in the aggregate”. That is, rather than executing the program on ordinary states, the program is executed on abstract states, which are finite-sized descriptors that represent collections of states.
However, there is a glitch: abstract interpretation has a well-deserved reputation of being a kind of “black art”, and consequently difficult to work with. In this talk, the speaker will describe a twenty-year quest to address this issue by raising the level of automation in abstract interpretation. He will also present several different approaches to creating correct-by-construction analyzers. Somewhat surprisingly, this research has recently allowed the speaker's group to establish connections between the problem and several other areas of computer science, including decision procedures, machine learning, knowledge compilation, data integration, and constraint programming.
About the speaker
Prof Thomas Reps received his PhD in Computer Science from Cornell University in 1982 and joined the University of Wisconsin-Madison in 1985. He is currently the J. Barkley Rosser Professor & Rajiv and Ritu Batra Chair in the Computer Sciences Department there.
Prof Reps’s research focuses on a wide variety of topics, including program slicing, dataflow analysis, pointer analysis, model checking, computer security, code instrumentation, language-based program-development environments, the use of program profiling in software testing, software renovation, incremental algorithms, and attribute grammars.
Prof Reps received numerous awards including NSF Presidential Young Investigator Award (1986), a Packard Fellowship (1988), a Humboldt Research Award (2000), and a Guggenheim Fellowship (2000). He was also elected as an ACM Fellow (2005). In 2013, Prof Reps was elected a foreign member of Academia Europaea.
|
