To refer to this page use:
|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.|
|Citation:||Kincaid, Zachary. "Numerical Invariants via Abstract Machines." In International Static Analysis Symposium (2018): pp. 24-42. doi:10.1007/978-3-319-99725-4_3|
|Pages:||24 - 42|
|Type of Material:||Conference Article|
|Journal/Proceeding Title:||International Static Analysis Symposium|
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.