Skip to Main content Skip to Navigation
New interface
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
Contributor : Fei He Connect in order to contact the contributor
Submitted on : Thursday, September 16, 2010 - 6:50:00 AM
Last modification on : Thursday, February 3, 2022 - 11:15:49 AM


  • HAL Id : inria-00517943, version 1



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⟩



Record views