An SMT Theory for n-Indexed Sequences
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916478240948224 |
|---|---|
| author | Hara, Hichem Rami Ait El Bobot, François Bury, Guillaume |
| author_facet | Hara, Hichem Rami Ait El Bobot, François Bury, Guillaume |
| contents | The SMT (Satisfiability Modulo Theories) theory of arrays is well-established and widely used, with variousdecision procedures and extensions developed for it. However, recent works suggest that developing tailoredreasoning for some theories, such as sequences and strings, is more efficient than reasoning over them throughaxiomatization over the theory of arrays. In this paper, we are interested in reasoning over n-indexed sequences asthey are found in some programming languages, such as Ada. We propose an SMT theory of n-indexed sequencesand explore different ways to represent and reason over n-indexed sequences using existing theories, as well astailored calculi for the theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_07665 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | An SMT Theory for n-Indexed Sequences Hara, Hichem Rami Ait El Bobot, François Bury, Guillaume Logic in Computer Science The SMT (Satisfiability Modulo Theories) theory of arrays is well-established and widely used, with variousdecision procedures and extensions developed for it. However, recent works suggest that developing tailoredreasoning for some theories, such as sequences and strings, is more efficient than reasoning over them throughaxiomatization over the theory of arrays. In this paper, we are interested in reasoning over n-indexed sequences asthey are found in some programming languages, such as Ada. We propose an SMT theory of n-indexed sequencesand explore different ways to represent and reason over n-indexed sequences using existing theories, as well astailored calculi for the theory. |
| title | An SMT Theory for n-Indexed Sequences |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2411.07665 |