W&M Featured Events
This calendar presented by
William & Mary
[PAST EVENT] Colloquium: Abstract Interpretation and Decision Procedures: Better Together!
March 6, 2014
8:30am - 9:30am
Aditya Thakur, University of Wisconsin, Madison
Abstract:
This talk explores the rich interplay between two areas of automated reasoning: static analysis of program, and decision procedures for logics. The goal of a program-analysis tool is to verify that a given program does not reach a bad state. It is impossible to establish full correctness of programs in general. Consequently, program-analysis tools work on an abstraction of a program, which over-approximates the original program's behavior. The theory underlying this approach is called abstract interpretation. Unfortunately, implementing a correct, precise, and scalable abstract interpreter has a well-deserved reputation of being a kind of "black art". In this talk, I describe how decision procedures can be used to raise the level of automation in abstract interpretation.
Moreover, the talk describes how concepts from abstract interpretation can be exploited to improve decision procedures. This new principle for designing decision procedures, which we call Satisfiability Modulo Abstraction, provides a way to create decision procedures for new logics.
Bio:
Aditya Thakur is a Ph.D. candidate in the Department of Computer Sciences at the University of Wisconsin-Madison. His research interests include program verification, decision procedures, and software engineering. He is the recipient of the 2013 Google Fellowship in Programming Technology.
Abstract:
This talk explores the rich interplay between two areas of automated reasoning: static analysis of program, and decision procedures for logics. The goal of a program-analysis tool is to verify that a given program does not reach a bad state. It is impossible to establish full correctness of programs in general. Consequently, program-analysis tools work on an abstraction of a program, which over-approximates the original program's behavior. The theory underlying this approach is called abstract interpretation. Unfortunately, implementing a correct, precise, and scalable abstract interpreter has a well-deserved reputation of being a kind of "black art". In this talk, I describe how decision procedures can be used to raise the level of automation in abstract interpretation.
Moreover, the talk describes how concepts from abstract interpretation can be exploited to improve decision procedures. This new principle for designing decision procedures, which we call Satisfiability Modulo Abstraction, provides a way to create decision procedures for new logics.
Bio:
Aditya Thakur is a Ph.D. candidate in the Department of Computer Sciences at the University of Wisconsin-Madison. His research interests include program verification, decision procedures, and software engineering. He is the recipient of the 2013 Google Fellowship in Programming Technology.