ng Abstract Interpretation Thomas Reps1,2 and Aditya Thakur3 1 University of Wisconsin; Madison, WI, USA 2 GrammaTech, Inc.; Ithaca, NY, USA 3 Google, Inc.; Mountain View, CA USA Abstract interpretation has a reputation of being a kind of “black art,” and consequently difficult to work with. This paper describes a twenty-year quest by the first author to address this issue by raising l of automation in abstract interpretation. The most recent leg of this journey is the subject of the second author’s 2014 Ph.D. dissertation. The paper discusses several different approaches to creating correct-by-construction analyzers. Our research has allowed us to establish connections between this problem and several other areas of computer science, including automated reasoning/decision procedures, concept learning, and constraint programming.
Thomas W. Reps, Aditya V. Thakur