Property-directed inference of relational invariants

D. A. Mordvinov

Modelirovanie i analiz informacionnyh sistem, Tome 26 (2019) no. 4, pp. 550-571.

Résumé

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.

Détail

Keywords: relational verification, constrained horn clauses, property-directed reachability
Mots-clés : relational invariants.

Bibliographie

[1] Krystof H., Bjørner N., “Generalized Property Directed Reachability”, LNCS, 7317, Springer, 2012, 157–171 | Zbl

[2] Cimatti A., Griggio A., Mover S., Tonetta S., “IC3 Modulo Theories via Implicit Predicate Abstraction”, LNCS, 8413, Springer, 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 | DOI | Zbl

[4] Jovanović D., Dutertre B., “Property-Directed $k$-induction”, FMCAD, IEEE, 2016, 85–92

[5] Fedyukovich G., Bodík R., “Accelerating Syntax-Guided Invariant Synthesis”, LNCS, 10805, Springer, 2018, 251–269

[6] Nepomniaschy V.A. et al., “Verification oriented language C-light”, Sb. Nauch. Tr. RAN, Sistemnaya Informatika, 9, Sib. Otd-nie. In-t Sistem Informatiki, 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 | DOI

[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, 9971, Springer, 2016, 149–165 | MR

[12] Beckert B., Bingmann T., Kiefer M., Sanders P., Ulbrich M., Weigl A., “Relational Equivalence Proofs Between Imperative and MapReduce Algorithms”, LNCS, 11294, Springer, 2018, 248–266

[13] Athanasiou K. et al., “SideTrail: Verifying Time-Balancing of Cryptosystems”, LNCS, 11294, Springer, 2018, 215–228

[14] Barthe G., Crespo J. M., Kunz C., “Relational Verification Using Product Programs”, LNCS, 6664, Springer, 2011, 200–214 | MR

[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, 9837, Springer, 2016, 147–169 | MR | Zbl

[17] Mordvinov D., Fedyukovich G., “Synchronizing Constrained Horn Clauses”, EPiC Series in Computing, EasyChair, 46 (2017), 338–355 | MR | Zbl

[18] Shemer R., Gurfinkel A., Shoham S., Vizel Y., “Property Directed Self Composition”, LNCS, 11561, Springer, 2019, 161–179 | MR

[19] Clarke E. M., “Program Invariants as Fixedpoints”, Computing, 21:4 (1979), 273–294 | DOI | MR | Zbl

[20] Apt K. R., From Logic Programming to Prolog, Prentice Hall, London, 1997

[21] Bjørner N., Janota M., “Playing with Quantified Satisfaction”, short papers, LPAR, 35 (2015), 15–27

[22] Bradley A. R., “SAT-Based Model Checking without Unrolling”, LNCS, 6538, Springer, 2011, 70–87 | MR | Zbl

[23] De Moura L., Bjørner N., “Z3: An Efficient SMT Solver”, LNCS, 4963, Springer, 2008, 337–340

[24] Mordvinov D., Fedyukovich G., Verifying Safety of Functional Programs with Rosette/Unbound, 2017, arXiv: 1704.04558 [cs.SE] | Zbl

[25] Strichman O., Veitsman M., “Regression Verification for Unbalanced Recursive Functions”, LNCS, 9995, 2016, 645–658 | MR | Zbl

[26] Sousa M., Dillig I., “Cartesian Hoare Logic for Verifying $k$-safety Properties”, PLDI, ACM, 2016, 57–69

[27] Pick L., Fedyukovich G., Gupta A., “Exploiting Synchrony and Symmetry in Relational Verification”, LNCS, 10981, Springer, 2018, 164–182 | MR