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.
Type de document :
Communication dans un congrès
CAV 2010 - 22nd International Conference on Computer Aided Verification, Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

https://hal.inria.fr/inria-00517943
Contributeur : Fei He <>
Soumis le : jeudi 16 septembre 2010 - 06:50:00
Dernière modification le : mardi 17 avril 2018 - 11:29:34

Identifiants

  • 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. 2010. 〈inria-00517943〉

Partager

Métriques

Consultations de la notice

224