Numerical Invariants via Abstract Machines

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 25th International Symposium, SAS 2018, Proceedings
EditorsAndreas Podelski
PublisherSpringer Verlag
Number of pages19
ISBN (Print)9783319997247
StatePublished - 2018
Event25th International Static Analysis Symposium, SAS 2018 - Freiburg, Germany
Duration: Aug 29 2018Aug 31 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11002 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other25th International Static Analysis Symposium, SAS 2018

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Numerical Invariants via Abstract Machines'. Together they form a unique fingerprint.

Cite this