Skip to main content

Numerical Invariants via Abstract Machines

Author(s): Kincaid, Zachary

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.
Publication Date: Aug-2018
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
DOI: 10.1007/978-3-319-99725-4_3
ISSN: 0302-9743
Pages: 24 - 42
Type of Material: Conference Article
Journal/Proceeding Title: International Static Analysis Symposium
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.