Sciweavers

Share
FMCAD
2009
Springer

Generalized, efficient array decision procedures

9 years 12 months ago
Generalized, efficient array decision procedures
Abstract--The theory of arrays is ubiquitous in the context of software and hardware verification and symbolic analysis. The basic array theory was introduced by McCarthy and allows to symbolically representing array updates. In this paper we present combinatory array logic, CAL, using a small, but powerful core of combinators, and reduce it to the theory of uninterpreted functions. CAL allows expressing properties that go well beyond the basic array theory. We provide a new efficient decision procedure for the base theory as well as CAL. The efficient procedure serves a critical role in the performance of the state-of-the-art SMT solver Z3 on array formulas from applications.
Leonardo Mendonça de Moura, Nikolaj Bj&osla
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2009
Where FMCAD
Authors Leonardo Mendonça de Moura, Nikolaj Bjørner
Comments (0)
books