Property-Directed Inference of Relational Invariants
Property Directed Reachability (PDR) is an efficient and scalable approach to solving systems of symbolic constraints also known as Constrained Horn Clauses (CHC). In the case of non-linear CHCs, which may arise, e.g., from relational verification tasks, PDR aims to infer an inductive invariant for...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2019-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1276 |
| _version_ | 1797877900334071808 |
|---|---|
| author | Dmitry A. Mordvinov |
| author_facet | Dmitry A. Mordvinov |
| author_sort | Dmitry A. Mordvinov |
| collection | DOAJ |
| description | Property Directed Reachability (PDR) is an efficient and scalable approach to solving systems of symbolic constraints also known as Constrained Horn Clauses (CHC). In the case of non-linear CHCs, which may arise, e.g., from relational verification tasks, PDR aims to infer an inductive invariant for each uninterpreted predicate. However, in many practical cases this reasoning is not successful, as invariants should be derived for groups of predicates instead of individual predicates. The article describes a novel algorithm that identifies these groups automatically and complements the existing PDR technique. The key feature of the algorithm is that it does not require a possibly expensive synchronization transformation over the system of CHCs. We have implemented the algorithm on top of a up-to-date CHC solver Spacer. Our experimental evaluation shows that for some CHC systems, on which existing solvers diverge, our tool is able to discover relational invariants. |
| first_indexed | 2024-04-10T02:24:17Z |
| format | Article |
| id | doaj.art-c386e4ad32d744e0bfa10a1efbfbffb8 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:24:17Z |
| publishDate | 2019-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-c386e4ad32d744e0bfa10a1efbfbffb82023-03-13T08:07:34ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172019-12-0126455057110.18255/1818-1015-2019-4-550-571953Property-Directed Inference of Relational InvariantsDmitry A. Mordvinov0JetBrains Research, Санкт-Петербургский государственный УниверситетProperty Directed Reachability (PDR) is an efficient and scalable approach to solving systems of symbolic constraints also known as Constrained Horn Clauses (CHC). In the case of non-linear CHCs, which may arise, e.g., from relational verification tasks, PDR aims to infer an inductive invariant for each uninterpreted predicate. However, in many practical cases this reasoning is not successful, as invariants should be derived for groups of predicates instead of individual predicates. The article describes a novel algorithm that identifies these groups automatically and complements the existing PDR technique. The key feature of the algorithm is that it does not require a possibly expensive synchronization transformation over the system of CHCs. We have implemented the algorithm on top of a up-to-date CHC solver Spacer. Our experimental evaluation shows that for some CHC systems, on which existing solvers diverge, our tool is able to discover relational invariants.https://www.mais-journal.ru/jour/article/view/1276реляционная верификациядизъюнкты хорна с ограниченияминаправляемая свойством достижимостьреляционные инварианты |
| spellingShingle | Dmitry A. Mordvinov Property-Directed Inference of Relational Invariants Моделирование и анализ информационных систем реляционная верификация дизъюнкты хорна с ограничениями направляемая свойством достижимость реляционные инварианты |
| title | Property-Directed Inference of Relational Invariants |
| title_full | Property-Directed Inference of Relational Invariants |
| title_fullStr | Property-Directed Inference of Relational Invariants |
| title_full_unstemmed | Property-Directed Inference of Relational Invariants |
| title_short | Property-Directed Inference of Relational Invariants |
| title_sort | property directed inference of relational invariants |
| topic | реляционная верификация дизъюнкты хорна с ограничениями направляемая свойством достижимость реляционные инварианты |
| url | https://www.mais-journal.ru/jour/article/view/1276 |
| work_keys_str_mv | AT dmitryamordvinov propertydirectedinferenceofrelationalinvariants |