From Traces to Program Incorrectness: A Type-Theoretic Approach
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914017402945536 |
|---|---|
| author | Yuan, Yongwei Zhou, Zhe Belyakova, Julia Delaware, Benjamin Jagannathan, Suresh |
| author_facet | Yuan, Yongwei Zhou, Zhe Belyakova, Julia Delaware, Benjamin Jagannathan, Suresh |
| contents | We present a type-theoretic framework for reasoning about incorrectness in functional programs that interact with effectful, opaque library APIs. Our approach centers on traces -- temporally-ordered sequences of library API invocations -- which naturally characterize both the preconditions of individual APIs and their composite behavior. We represent these traces using symbolic regular expressions (SREs), enabling formal specification of incorrect abstract data type (ADT) behaviors across function boundaries. The core contribution is a novel type inference algorithm that operates modulo specified incorrectness properties and leverages the symbolic finite automata (SFAs) representations of regexes for compositional reasoning of traces. When the algorithm succeeds, the inferred types witness that an ADT implementation can exhibit some subset of the specified incorrect behaviors. This represents the first systematic approach to underapproximate reasoning against trace-based incorrectness specifications, enabling a new form of trace-guided compositional analysis. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_02428 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | From Traces to Program Incorrectness: A Type-Theoretic Approach Yuan, Yongwei Zhou, Zhe Belyakova, Julia Delaware, Benjamin Jagannathan, Suresh Programming Languages We present a type-theoretic framework for reasoning about incorrectness in functional programs that interact with effectful, opaque library APIs. Our approach centers on traces -- temporally-ordered sequences of library API invocations -- which naturally characterize both the preconditions of individual APIs and their composite behavior. We represent these traces using symbolic regular expressions (SREs), enabling formal specification of incorrect abstract data type (ADT) behaviors across function boundaries. The core contribution is a novel type inference algorithm that operates modulo specified incorrectness properties and leverages the symbolic finite automata (SFAs) representations of regexes for compositional reasoning of traces. When the algorithm succeeds, the inferred types witness that an ADT implementation can exhibit some subset of the specified incorrect behaviors. This represents the first systematic approach to underapproximate reasoning against trace-based incorrectness specifications, enabling a new form of trace-guided compositional analysis. |
| title | From Traces to Program Incorrectness: A Type-Theoretic Approach |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2509.02428 |