Incrementalizing Abstract Interpretation

Research output: Chapter in Book/Report/Conference proceedingMeeting abstract (Book)


A powerful approach to design static analysers is abstract interpretation, which reasons over an approximation of the program’s behaviour. The Abstracting Abstract Machines (AAM) technique, introduced by Van Horn & Might, presents a systematic approach to derive abstract interpreters. However, it is often not useable in the development and evolution of large- scale applications, as with the current state-of-the-art, an AAM analysis can not incrementally update its results upon changes in the program. That is, whenever minor modifications occur in the program’s source code, one needs to recompute the entire AAM analysis from scratch, which can easily get time-consuming.We therefore propose an incremental approach to abstract interpretation, more precisely the AAM technique. That is, we modify the technique so that the result of an AAM analysis, the abstract state graph, can incrementally be updated following a change in the program’s source code. Our algorithm tracks dependencies between the nodes in the abstract syntax tree (AST) of the program and the transitions in the abstract state graph to invalidate and recompute new transitions in the state graph upon a change in the AST. Our experiments using a set of Scheme micro-benchmarks reveal that in practice this approach is often limited, as only states that are identical in both state graphs are reusable. We therefore introduce an improvement to the original incremental algorithm, which we refer to as state adaptation. State adaptation also enables reusing states that are not identical, but similar. Both the original and improved algorithm are integrated and evaluated in the Scala-AM framework. Our current implementations already show good results in terms of incremental efficiency, although more optimization is required to achieve actual gains in run time performance with our approaches.
Original languageEnglish
Title of host publicationProceedings of the 16th edition of the BElgian-NEtherlands software eVOLution symposium
EditorsSerge Demeyer, Ali Parsai, Gulsher Laghari, Brent van Bladel
PublisherCEUR Workshop Proceedings
Number of pages5
ISBN (Electronic)1613-0073
Publication statusPublished - 11 Jan 2018
EventBElgian-NEtherlands software eVOLution symposium 2017 (BENEVOL) - Hof Van Liere - Prinsstraat 13 - BE 2000 Antwerp (Belgium), Antwerp, Belgium
Duration: 4 Dec 20175 Dec 2017

Publication series

ISSN (Electronic)1613-0073


WorkshopBElgian-NEtherlands software eVOLution symposium 2017 (BENEVOL)
Abbreviated titleBENEVOL 2017
Internet address


  • AAM
  • Abstract interpretation
  • Incremental computation
  • Static analysis


Dive into the research topics of 'Incrementalizing Abstract Interpretation'. Together they form a unique fingerprint.

Cite this