Second-Order Value Numbering

Authors

  • Tiziana Margaria
  • Bernhard Steffen
  • Christian Topnik

DOI:

https://doi.org/10.14279/tuj.eceasst.30.439

Abstract

We present second-order value numbering, a new optimization method for suppressing redundancy, in a version tailored to the application for optimizing the decision procedure of jMosel, a verification tool set for monadic second-order logic on strings (M2L(Str)). The method extends the well-known concept of value numbering to consider not merely values, but semantics transformers that can be efficiently pre-computed and help to avoid redundancy at the 2nd-order level. Since decision procedures for M2L are non-elementary, an optimization method like this can have a great impact on the execution time, even though our decision procedure comprises the analysis and optimization time for second-order value numbering. This is illustrated considering a parametric family of hardware circuits, where we observed a performance gain by a factor of 3. This result is surprising, as the design of these circuits exploits already structural similarity.

Downloads

Published

2010-11-08

How to Cite

[1]
T. Margaria, B. Steffen, and C. Topnik, “Second-Order Value Numbering”, eceasst, vol. 30, Nov. 2010.