Property-Directed Inference of Relational Invariants
https://doi.org/10.18255/1818-1015-2019-4-550-571
Abstract
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.
Keywords
relational verification,
constrained horn clauses,
property-directed reachability,
relational invariants
Supporting agencies: This work was supported by JetBrains Research.
About the Author
Dmitry A. Mordvinov
JetBrains Research, St Petersburg University
Russian Federation
senior reseacher
Russian Federation
senior reseacher
References
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. 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).
7. Mandrykin M. U., Mutilin V. S., Khoroshilov A. V., “Introduction to CEGAR — Counter-Example Guided Abstraction Refinement”, Proceedings of ISP RAS, 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.
Review
For citations:
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
Views:
679
Email this article 