maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2019-4-550-571mais-1276Research ArticleAlgorithmsНаправляемый свойством поиск реляционных инвариантовProperty-Directed Inference of Relational Invariantshttps://orcid.org/0000-0002-6437-3020МордвиновДмитрий АлександровичMordvinovDmitry A.

стар. преп.

senior reseacher

dmitry.mordvinov@jetbrains.comJetBrains Research, Санкт-Петербургский государственный УниверситетРоссияJetBrains Research, St Petersburg UniversityRussian Federation201913122019264550571Copyright © Мордвинов Д.А., 20192019Мордвинов Д.А.Mordvinov D.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1276

Достижимость, направляемая свойством, (Property Directed Reachability, PDR) — эффективный и масштабируемый подход к решению систем символьных ограничений, известных как дизъюнкты Хорна с ограничениями (Constrained Horn Clauses, CHC). В случае нелинейных систем дизъюнктов, которые могут возникнуть, к примеру, из задач реляционной верификации, PDR выводит индуктивные инварианты для каждого неинтерпретированного предикатного символа. Тем не менее на практике автоматический вывод таких решений не удаётся, т.к. инварианты должны выводиться для групп предикатных символов вместо индивидуальных предикатных символов. В статье описан новый алгоритм, автоматически определяющий такие группы и обобщающий существующий подход PDR. Ключевая особенность алгоритма состоит в том, что он не требует потенциально дорогой синхронизирующей трансформации системы дизъюнктов Хорна. Алгоритм был реализован над современным решателем дизъюнктов Хорна Spacer. Эксперименты показывают, что полученная реализация успешно выводит реляционные инварианты для некоторых систем дизъюнктов, на которых существующие решатели не завершаются.

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.

реляционная верификациядизъюнкты Хорна с ограниченияминаправляемая свойством достижимостьреляционные инвариантыrelational verificationconstrained horn clausesproperty-directed reachabilityrelational invariantsРабота выполнена при финансовой поддержке JetBrains Research.This work was supported by JetBrains Research.ReferencesKrystof H., Bjørner N, “Generalized Property Directed Reachability”, LNCS, Springer, 7317 (2012), 157–171.Krystof H., Bjørner N, “Generalized Property Directed Reachability”, LNCS, Springer, 7317 (2012), 157–171.Cimatti A., Griggio A., Mover S., Tonetta S., “IC3 Modulo Theories via Implicit Predicate Abstraction”, LNCS, Springer, 8413 (2014), 46–61.Cimatti A., Griggio A., Mover S., Tonetta S., “IC3 Modulo Theories via Implicit Predicate Abstraction”, LNCS, Springer, 8413 (2014), 46–61.Komuravelli A., Gurfinkel A., Chaki S., “SMT-Based Model Checking for Recursive Programs”, Formal Methods in System Design, 48:3 (2016), 175–205.Komuravelli A., Gurfinkel A., Chaki S., “SMT-Based Model Checking for Recursive Programs”, Formal Methods in System Design, 48:3 (2016), 175–205.Jovanovi´c D., Dutertre B., “Property-Directed ????-induction”, FMCAD,IEEE, 2016, 85–92.Jovanovi´c D., Dutertre B., “Property-Directed ????-induction”, FMCAD,IEEE, 2016, 85–92.Fedyukovich G., Bod´ık R., “Accelerating Syntax-Guided Invariant Synthesis”, LNCS, Springer, 10805 (2018), 251–269.Fedyukovich G., Bod´ık R., “Accelerating Syntax-Guided Invariant Synthesis”, LNCS, Springer, 10805 (2018), 251–269.Непомнящий В.А. и др., “Ориентированный на верификацию язык C-light”, Системная информатика: Сб. науч. тр. РАН. Сиб. отд-ние. Ин-т систем информатики, 9 (2004), 51–134.Nepomniaschy V.A. et al., “Verification oriented language C-light”, Sistemnaya Informatika: Sb. Nauch. Tr. RAN. Sib. Otd-nie. In-t Sistem Informatiki, 9 (2004), 51–134, (in Russian).Мандрыкин М. У., Мутилин В. С., Хорошилов А. В., “Введение в метод CEGAR — уточнение абстракции по контрпримерам”, Труды Института системного программирования РАН, 24 (2013).Mandrykin M. U., Mutilin V. S., Khoroshilov A. V., “Introduction to CEGAR — Counter-Example Guided Abstraction Refinement”, Proceedings of ISP RAS, 24 2013.Champion A., Kobayashi N., Sato R., “HoIce: An ICE-Based Non-linear Horn Clause Solver”, Asian Symposium on Programming Languages and Systems, Springer, 2018, 146– 156.Champion A., Kobayashi N., Sato R., “HoIce: An ICE-Based Non-linear Horn Clause Solver”, Asian Symposium on Programming Languages and Systems, Springer, 2018, 146– 156.Lahiri S. K., McMillan K. L., Sharma R., Hawblitzel C., “Differential Assertion Checking”, FSE, ACM, 2013, 345–355.Lahiri S. K., McMillan K. L., Sharma R., Hawblitzel C., “Differential Assertion Checking”, FSE, ACM, 2013, 345–355.Almeida J. B., Barbosa M., Barthe G., Dupressoir F., Emmi M., “Verifying Constant-Time Implementations”, USENIX, 2016, 53–70.Almeida J. B., Barbosa M., Barthe G., Dupressoir F., Emmi M., “Verifying Constant-Time Implementations”, USENIX, 2016, 53–70.Kiefer M., Klebanov V., Ulbrich M., “Relational Program Reasoning Using Compiler IR”, LNCS, Springer, 9971 (2016), 149–165.Kiefer M., Klebanov V., Ulbrich M., “Relational Program Reasoning Using Compiler IR”, LNCS, Springer, 9971 (2016), 149–165.Beckert B., Bingmann T., Kiefer M., Sanders P., Ulbrich M., Weigl A., “Relational Equivalence Proofs Between Imperative and MapReduce Algorithms”, LNCS, Springer, 11294 (2018), 248–266.Beckert B., Bingmann T., Kiefer M., Sanders P., Ulbrich M., Weigl A., “Relational Equivalence Proofs Between Imperative and MapReduce Algorithms”, LNCS, Springer, 11294 (2018), 248–266.Athanasiou K. et al., “SideTrail: Verifying Time-Balancing of Cryptosystems”, LNCS, Springer, 11294 (2018), 215–228.Athanasiou K. et al., “SideTrail: Verifying Time-Balancing of Cryptosystems”, LNCS, Springer, 11294 (2018), 215–228.Barthe G., Crespo J. M., Kunz C., “Relational Verification Using Product Programs”, LNCS, Springer, 6664 (2011), 200–214.Barthe G., Crespo J. M., Kunz C., “Relational Verification Using Product Programs”, LNCS, Springer, 6664 (2011), 200–214.Felsing D. et al., “Automating Regression Verification”, ASE, ACM, 2014, 349–360.Felsing D. et al., “Automating Regression Verification”, ASE, ACM, 2014, 349–360.De Angelis E. et al., “Relational Verification Through Horn Clause Transformation”, LNCS, Springer, 9837 (2016), 147–169.De Angelis E. et al., “Relational Verification Through Horn Clause Transformation”, LNCS, Springer, 9837 (2016), 147–169.Mordvinov D., Fedyukovich G., “Synchronizing Constrained Horn Clauses”, EPiC Series in Computing, EasyChair, 46 (2017), 338–355.Mordvinov D., Fedyukovich G., “Synchronizing Constrained Horn Clauses”, EPiC Series in Computing, EasyChair, 46 (2017), 338–355.Shemer R., Gurfinkel A., Shoham S., Vizel Y., “Property Directed Self Composition”, LNCS, Springer, 11561 (2019), 161–179.Shemer R., Gurfinkel A., Shoham S., Vizel Y., “Property Directed Self Composition”, LNCS, Springer, 11561 (2019), 161–179.Clarke E. M., “Program Invariants as Fixedpoints”, 21:4 (1979), 273–294.Clarke E. M., “Program Invariants as Fixedpoints”, 21:4 (1979), 273–294.Apt K. R., From Logic Programming to Prolog, Prentice Hall London, 1997.Apt K. R., From Logic Programming to Prolog, Prentice Hall London, 1997.Bjørner N., Janota M., “Playing with Quantified Satisfaction”, LPAR (short papers), 35 (2015), 15–27.Bjørner N., Janota M., “Playing with Quantified Satisfaction”, LPAR (short papers), 35 (2015), 15–27.Bradley A. R., “SAT-Based Model Checking without Unrolling”, LNCS, Springer, 6538 (2011), 70–87.Bradley A. R., “SAT-Based Model Checking without Unrolling”, LNCS, Springer, 6538 (2011), 70–87.De Moura L., Bjørner N., “Z3: An Efficient SMT Solver”, LNCS, Springer, 4963 (2008), 337–340.De Moura L., Bjørner N., “Z3: An Efficient SMT Solver”, LNCS, Springer, 4963 (2008), 337–340.Mordvinov D., Fedyukovich G., “Verifying Safety of Functional Programs with Rosette/Unbound”, CoRR., abs/1704.04558. (2017).Mordvinov D., Fedyukovich G., “Verifying Safety of Functional Programs with Rosette/Unbound”, CoRR., abs/1704.04558. (2017).Strichman O., Veitsman M., “Regression Verification for Unbalanced Recursive Functions”, LNCS, 9995 (2016), 645–658.Strichman O., Veitsman M., “Regression Verification for Unbalanced Recursive Functions”, LNCS, 9995 (2016), 645–658.Sousa M., Dillig I., “Cartesian Hoare Logic for Verifying ????-safety Properties”, PLDI, ACM, 2016, 57–69.Sousa M., Dillig I., “Cartesian Hoare Logic for Verifying ????-safety Properties”, PLDI, ACM, 2016, 57–69.Pick L., Fedyukovich G., Gupta A., “Exploiting Synchrony and Symmetry in Relational Verification”, LNCS, Springer, 10981 (2018), 164–182.Pick L., Fedyukovich G., Gupta A., “Exploiting Synchrony and Symmetry in Relational Verification”, LNCS, Springer, 10981 (2018), 164–182.

The authors declare that there are no conflicts of interest present.