Paper Info
Title
Array Theory of Bounded Elements and its Applications
Abstract
We investigate a first-order array theory of bounded elements. This theory has rich expressive power that allows free use of quantifiers. By reducing to weak second-order logic with one successor (WS1S), we show that the proposed array theory is decidable. Then two natural extensions to the new theory are shown to be undecidable. A translation-based decision procedure for this theory is implemented, and is shown applicable to program verification.
Year
DOI
Venue
2014
10.1007/s10817-013-9293-6
J. Autom. Reasoning
Keywords
Field
DocType
Satisfiability modulo theories,Array theory,Program verification
Discrete mathematics,Successor cardinal,Algorithm,C-minimal theory,Decidability,Expressive power,Mathematics,Undecidable problem,Bounded function,Satisfiability modulo theories
Journal
Volume
Issue
ISSN
52
4
0168-7433
Citations 
PageRank 
References 
4
0.43
21
Authors
5
Name
Order
Citations
PageRank
Min Zhou16922.62
Fei He217528.32
Bow-yaw Wang323425.60
Ming Gu455474.82
Jia-guang Sun51807134.30