Research

Abstract Acceleration

Acceleration methods are used to speed up the convergence of analysis algorithms in the presence of loops in program analysed. Acceleration methods compute the effect of loops non-iteratively by considering closed forms for an (potentially) unbounded number of iterations of the loop. Abstract acceleration aims at computing precise over-approximations of the collecting semantics by abstracting the closed form in an abstract domain.

The original idea for abstract acceleration was presented by Gonnord and Halbwachs for closed linear systems whose transitions have the finite monoid property.
  • Laure Gonnord and Peter Schrammel. Abstract Acceleration in Linear Relation Analysis. Science of Computer Programming, 93:125-153, 2014. [bibtex] [link]
gives a survey and introduction into the foundations of the topic.

The publications below describe recent research and extensions of the original technique:
  • Peter Schrammel: Unbounded-time reachability analysis of hybrid systems by abstract acceleration. In Embedded Software, EMSOFT'15, pp. 51-54, IEEE, 2015. [bibtex] [link]
  • Dario Cattaruzza, Alessandro Abate, Peter Schrammel, Daniel Kroening: Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration. In Static analysis, SAS'15, pp. 312-331, Springer, 2015. [bibtex] [experiments] [link]
  • Bertrand Jeannet, Peter Schrammel and Sriram Sankaranarayanan. Abstract Acceleration of General Linear Loops. In Principles of Programming Languages, POPL'14, pp. 529-540, ACM, 2014. [bibtex] [experiments] [link]
  • Peter Schrammel. Logico-Numerical Verification Methods for Discrete and Hybrid Systems. PhD Thesis, University of Grenoble, France. [bibtex] [pdf]
  • Peter Schrammel and Bertrand Jeannet. Applying Abstract Acceleration to (Co-)Reachability Analysis of Reactive Programs. Journal of Symbolic Computation, 47(12):1512-1532, 2012. [bibtex] [link]
  • Peter Schrammel and Bertrand Jeannet. Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs. In Static Analysis, SAS'11. Vol. 6887 of LNCS, pp. 233-248, Springer, 2011. [bibtex] [link]
  • Peter Schrammel and Bertrand Jeannet. Extending Abstract Acceleration to Data-Flow Programs with Numerical Inputs. In Numerical and Symbolic Abstract Domains, NSAD'10. Vol. 267 of ENTCS, pp. 101-114, Elsevier, 2010. [bibtex] [link]

Peter
Schrammel

Research Interests

Biography

Software