Направляемый свойством поиск реляционных инвариантов
https://doi.org/10.18255/1818-1015-2019-4-550-571
Аннотация
Достижимость, направляемая свойством, (Property Directed Reachability, PDR) — эффективный и масштабируемый подход к решению систем символьных ограничений, известных как дизъюнкты Хорна с ограничениями (Constrained Horn Clauses, CHC). В случае нелинейных систем дизъюнктов, которые могут возникнуть, к примеру, из задач реляционной верификации, PDR выводит индуктивные инварианты для каждого неинтерпретированного предикатного символа. Тем не менее на практике автоматический вывод таких решений не удаётся, т.к. инварианты должны выводиться для групп предикатных символов вместо индивидуальных предикатных символов. В статье описан новый алгоритм, автоматически определяющий такие группы и обобщающий существующий подход PDR. Ключевая особенность алгоритма состоит в том, что он не требует потенциально дорогой синхронизирующей трансформации системы дизъюнктов Хорна. Алгоритм был реализован над современным решателем дизъюнктов Хорна Spacer. Эксперименты показывают, что полученная реализация успешно выводит реляционные инварианты для некоторых систем дизъюнктов, на которых существующие решатели не завершаются.
Ключевые слова
реляционная верификация,
дизъюнкты Хорна с ограничениями,
направляемая свойством достижимость,
реляционные инварианты
При поддержке: Работа выполнена при финансовой поддержке JetBrains Research.
Об авторе
Дмитрий Александрович Мордвинов
JetBrains Research, Санкт-Петербургский государственный Университет
Россия
стар. преп.
Россия
стар. преп.
Список литературы
1. Krystof H., Bjørner N, “Generalized Property Directed Reachability”, LNCS, Springer, 7317 (2012), 157–171.
2. Cimatti A., Griggio A., Mover S., Tonetta S., “IC3 Modulo Theories via Implicit Predicate Abstraction”, LNCS, Springer, 8413 (2014), 46–61.
3. Komuravelli A., Gurfinkel A., Chaki S., “SMT-Based Model Checking for Recursive Programs”, Formal Methods in System Design, 48:3 (2016), 175–205.
4. Jovanovi´c D., Dutertre B., “Property-Directed ????-induction”, FMCAD,IEEE, 2016, 85–92.
5. Fedyukovich G., Bod´ık R., “Accelerating Syntax-Guided Invariant Synthesis”, LNCS, Springer, 10805 (2018), 251–269.
6. Непомнящий В.А. и др., “Ориентированный на верификацию язык C-light”, Системная информатика: Сб. науч. тр. РАН. Сиб. отд-ние. Ин-т систем информатики, 9 (2004), 51–134.
7. Мандрыкин М. У., Мутилин В. С., Хорошилов А. В., “Введение в метод CEGAR — уточнение абстракции по контрпримерам”, Труды Института системного программирования РАН, 24 (2013).
8. 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.
9. Lahiri S. K., McMillan K. L., Sharma R., Hawblitzel C., “Differential Assertion Checking”, FSE, ACM, 2013, 345–355.
10. Almeida J. B., Barbosa M., Barthe G., Dupressoir F., Emmi M., “Verifying Constant-Time Implementations”, USENIX, 2016, 53–70.
11. Kiefer M., Klebanov V., Ulbrich M., “Relational Program Reasoning Using Compiler IR”, LNCS, Springer, 9971 (2016), 149–165.
12. 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.
13. Athanasiou K. et al., “SideTrail: Verifying Time-Balancing of Cryptosystems”, LNCS, Springer, 11294 (2018), 215–228.
14. Barthe G., Crespo J. M., Kunz C., “Relational Verification Using Product Programs”, LNCS, Springer, 6664 (2011), 200–214.
15. Felsing D. et al., “Automating Regression Verification”, ASE, ACM, 2014, 349–360.
16. De Angelis E. et al., “Relational Verification Through Horn Clause Transformation”, LNCS, Springer, 9837 (2016), 147–169.
17. Mordvinov D., Fedyukovich G., “Synchronizing Constrained Horn Clauses”, EPiC Series in Computing, EasyChair, 46 (2017), 338–355.
18. Shemer R., Gurfinkel A., Shoham S., Vizel Y., “Property Directed Self Composition”, LNCS, Springer, 11561 (2019), 161–179.
19. Clarke E. M., “Program Invariants as Fixedpoints”, 21:4 (1979), 273–294.
20. Apt K. R., From Logic Programming to Prolog, Prentice Hall London, 1997.
21. Bjørner N., Janota M., “Playing with Quantified Satisfaction”, LPAR (short papers), 35 (2015), 15–27.
22. Bradley A. R., “SAT-Based Model Checking without Unrolling”, LNCS, Springer, 6538 (2011), 70–87.
23. De Moura L., Bjørner N., “Z3: An Efficient SMT Solver”, LNCS, Springer, 4963 (2008), 337–340.
24. Mordvinov D., Fedyukovich G., “Verifying Safety of Functional Programs with Rosette/Unbound”, CoRR., abs/1704.04558. (2017).
25. Strichman O., Veitsman M., “Regression Verification for Unbalanced Recursive Functions”, LNCS, 9995 (2016), 645–658.
26. Sousa M., Dillig I., “Cartesian Hoare Logic for Verifying ????-safety Properties”, PLDI, ACM, 2016, 57–69.
27. Pick L., Fedyukovich G., Gupta A., “Exploiting Synchrony and Symmetry in Relational Verification”, LNCS, Springer, 10981 (2018), 164–182.
Рецензия
Для цитирования:
Мордвинов Д.А. Направляемый свойством поиск реляционных инвариантов. Моделирование и анализ информационных систем. 2019;26(4):550-571. https://doi.org/10.18255/1818-1015-2019-4-550-571
For citation:
Mordvinov D.A. Property-Directed Inference of Relational Invariants. Modeling and Analysis of Information Systems. 2019;26(4):550-571. (In Russ.) https://doi.org/10.18255/1818-1015-2019-4-550-571
Просмотров:
665
Послать статью по эл. почте 