Skip to Main content Skip to Navigation
Conference papers

On Array Theory of Bounded Elements

Min Zhou 1 Fei He 1, 2 Bow-Yaw Wang 2 Ming Gu 2
2 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : We investigate a first-order array theory of bounded elements. By reducing to weak second-order logic with one successor (WS1S), we show that the proposed array theory is decidable. Finally, two natural extensions to the new theory are shown to be undecidable.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00517943
Contributor : Fei He <>
Submitted on : Thursday, September 16, 2010 - 6:50:00 AM
Last modification on : Wednesday, June 2, 2021 - 3:39:58 AM

Identifiers

  • HAL Id : inria-00517943, version 1

Collections

Citation

Min Zhou, Fei He, Bow-Yaw Wang, Ming Gu. On Array Theory of Bounded Elements. CAV 2010 - 22nd International Conference on Computer Aided Verification, Jul 2010, Edinburgh, United Kingdom. ⟨inria-00517943⟩

Share

Metrics

Record views

547