HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols

Vlad Rusu 1
1 PAMPA - Models and Tools for Programming Distributed Parallel Architectures
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : We study a class of extended automata defined by guarded commands over Presburger arithmetic with uninterpreted functions. On the theoretical side, we show that the bounded reachability problem is decidable in this model. On the practical side, the class is useful for modeling programs with potentially infinite data structures, and the reachability procedure can be used for symbolic simulation, testing, and verification.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 10:11:53 AM
Last modification on : Friday, February 4, 2022 - 3:16:39 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:12:17 PM


  • HAL Id : inria-00072531, version 1


Vlad Rusu. Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols. [Research Report] RR-4100, INRIA. 2001. ⟨inria-00072531⟩



Record views


Files downloads