Reasoning over n-indexed sequences in SMT
Abstract The SMT (Satisfiability Modulo Theories) theory of arrays is well-established and widely used, with various decision procedures and extensions developed for it. However, recent contributions suggest that developing tailored reasoning for some theories, such as sequences and strings, can be more efficient than reasoning over them through axiomatization over the theory of arrays. In this paper, we are interested in reasoning over $$n$$ -indexed sequences as they are found in some programming languages, such as Ada. We propose an SMT theory of $$n$$ -indexed sequences and explore different ways to represent and reason over $$n$$ -indexed sequences using existing theories, as well as tailored calculi for this theory.
Authors
- Hichem Rami Ait El Hara (ORCID: https://orcid.org/0000-0001-7909-0413)
- François Bobot (ORCID: https://orcid.org/0000-0002-6756-0788)
- Guillaume Bury (ORCID: https://orcid.org/0009-0002-1267-251X)
Institutions
- Organisation de Coopération et de Développement Economiques (FR)
- Commissariat à l'Énergie Atomique et aux Énergies Alternatives (FR)
- Université Paris-Saclay (FR)
- Laboratoire d'Intégration des Systèmes et des Technologies (FR)
Publication Details
- Journal
- Acta Informatica
- Published
- 2025-08-21
- DOI
- https://doi.org/10.1007/s00236-025-00496-w
- Primary Topic
- Logic, programming, and type systems
- Type
- article
- Field-Weighted Citation Impact
- 0.00
Funders
- Université Paris-Saclay