@inproceedings{832d0b6f83fd482785ae9862dd869f4e,
title = "Numerical Invariants via Abstract Machines",
abstract = "This paper presents an overview of a line of recent work on generating non-linear numerical invariants for loops and recursive procedures. The method is compositional in the sense that it operates by breaking the program into parts, analyzing each part independently, and then combining the results. The fundamental challenge is to devise an effective method for analyzing the behavior of a loop given the results of analyzing its body. The key idea is to separate the problem into two: first we approximate the loop dynamics by an abstract machine, and then symbolically compute the reachability relation of the abstract machine.",
author = "Zachary Kincaid",
note = "Publisher Copyright: {\textcopyright} 2018, Springer Nature Switzerland AG.; 25th International Static Analysis Symposium, SAS 2018 ; Conference date: 29-08-2018 Through 31-08-2018",
year = "2018",
doi = "10.1007/978-3-319-99725-4_3",
language = "English (US)",
isbn = "9783319997247",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "24--42",
editor = "Andreas Podelski",
booktitle = "Static Analysis - 25th International Symposium, SAS 2018, Proceedings",
address = "Germany",
}