Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
Beyond the elementary representations of program invariants over algebraic data types. / Kostyukov, Yurii; Mordvinov, Dmitry; Fedyukovich, Grigory.
PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ed. / Stephen N. Freund; Eran Yahav. Association for Computing Machinery, 2021. p. 451-465 (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
}
TY - GEN
T1 - Beyond the elementary representations of program invariants over algebraic data types
AU - Kostyukov, Yurii
AU - Mordvinov, Dmitry
AU - Fedyukovich, Grigory
N1 - Publisher Copyright: © 2021 ACM.
PY - 2021/6/18
Y1 - 2021/6/18
N2 - First-order logic is a natural way of expressing properties of computation. It is traditionally used in various program logics for expressing the correctness properties and certificates. Although such representations are expressive for some theories, they fail to express many interesting properties of algebraic data types (ADTs). In this paper, we explore three different approaches to represent program invariants of ADT-manipulating programs: tree automata, and first-order formulas with or without size constraints. We compare the expressive power of these representations and prove the negative definability of both first-order representations using the pumping lemmas. We present an approach to automatically infer program invariants of ADT-manipulating programs by a reduction to a finite model finder. The implementation called RInGen has been evaluated against state-of-the-art invariant synthesizers and has been experimentally shown to be competitive. In particular, program invariants represented by automata are capable of expressing more complex properties of computation and their automatic construction is often less expensive.
AB - First-order logic is a natural way of expressing properties of computation. It is traditionally used in various program logics for expressing the correctness properties and certificates. Although such representations are expressive for some theories, they fail to express many interesting properties of algebraic data types (ADTs). In this paper, we explore three different approaches to represent program invariants of ADT-manipulating programs: tree automata, and first-order formulas with or without size constraints. We compare the expressive power of these representations and prove the negative definability of both first-order representations using the pumping lemmas. We present an approach to automatically infer program invariants of ADT-manipulating programs by a reduction to a finite model finder. The implementation called RInGen has been evaluated against state-of-the-art invariant synthesizers and has been experimentally shown to be competitive. In particular, program invariants represented by automata are capable of expressing more complex properties of computation and their automatic construction is often less expensive.
KW - algebraic data types
KW - finite models
KW - first-order definability
KW - invariant representation
KW - invariants
KW - tree automata
UR - http://www.scopus.com/inward/record.url?scp=85108910686&partnerID=8YFLogxK
UR - https://www.mendeley.com/catalogue/26a6e626-0765-3674-aecc-8ac2061bc9f2/
U2 - 10.1145/3453483.3454055
DO - 10.1145/3453483.3454055
M3 - Conference contribution
AN - SCOPUS:85108910686
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 451
EP - 465
BT - PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
A2 - Freund, Stephen N.
A2 - Yahav, Eran
PB - Association for Computing Machinery
T2 - 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021
Y2 - 20 June 2021 through 25 June 2021
ER -
ID: 85230750