Направляемый свойством поиск реляционных инвариантов
https://doi.org/10.18255/1818-1015-2019-4-550-571
Аннотация
Ключевые слова
Об авторе
Дмитрий Александрович МордвиновРоссия
стар. преп.
Список литературы
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