Presenter
Roland Graf
University of Regensburg
Authors
Philipp Rümmer, Roland Graf
Abstract
In formal software verification, SMT solvers play an important role. They act as the backend of verification queries. The availability of decidable theories and efficient decision procedures is therefore crucial. One such theory is the theory of arrays defined by read and write. Several extensions have been studied in the past, including combinatory array logic, array folds logic or cartesian array logic. However, theories that support summation over arrays have received little attention so far. Only recently has this extension been investigated. The talk presents the theory extension by sum constraints. Particular focus is placed on the connection to LIA*, a theory extension of linear integer arithmetic by a star operator that allows constraints about the possible result of an iterated summation process over a set. It is shown how both arrays with bounded sums and arrays with unbounded sums can be reduced to LIA* and, consequently, decided in nondeterministic polynomial time.
Slides
TBA