Abstract Predicate Entailment over Points-To Heaplets is Syntax Recognition
Logic in Computer Science
2019-06-04 v1 Formal Languages and Automata Theory
Symbolic Computation
Abstract
Abstract predicates are considered in this paper as abstraction technique for heap-separated configurations, and as genuine Prolog predicates which are translated straight into a corresponding formal language grammar used as validation scheme for intermediate heap states. The approach presented is rule-based because the abstract predicates are rule-based, the parsing technique can be interpreted as an automated fold/unfold of the corresponding heap graph.
Cite
@article{arxiv.1906.00217,
title = {Abstract Predicate Entailment over Points-To Heaplets is Syntax Recognition},
author = {René Haberland and Kirill Krinkin and Sergey Ivanovskiy},
journal= {arXiv preprint arXiv:1906.00217},
year = {2019}
}
Comments
9 pages, 3 figures