Geodesic
Property-directed inference of relational invariants
Modelirovanie i analiz informacionnyh sistem, Tome 26 (2019) no. 4, pp. 550-571

Voir la notice de l'article provenant de la source Math-Net.Ru

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
Mots-clés : relational invariants. 
@article{MAIS_2019_26_4_a6,
     author = {D. A. Mordvinov},
     title = {Property-directed inference of relational invariants},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {550--571},
     publisher = {mathdoc},
     volume = {26},
     number = {4},
     year = {2019},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a6/}
}
TY  - JOUR
AU  - D. A. Mordvinov
TI  - Property-directed inference of relational invariants
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2019
SP  - 550
EP  - 571
VL  - 26
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a6/
LA  - ru
ID  - MAIS_2019_26_4_a6
ER  - 
%0 Journal Article
%A D. A. Mordvinov
%T Property-directed inference of relational invariants
%J Modelirovanie i analiz informacionnyh sistem
%D 2019
%P 550-571
%V 26
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a6/
%G ru
%F MAIS_2019_26_4_a6
D. A. Mordvinov. Property-directed inference of relational invariants. Modelirovanie i analiz informacionnyh sistem, Tome 26 (2019) no. 4, pp. 550-571. http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a6/