Paper: Oct 13,2024
cs.PL
ID:2410.09668
Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
Verifying programs that manipulate tree data structures often requires
complex, ad-hoc proofs that are hard to generalize and automate. This paper
introduces an automatic technique for analyzing such programs. Our approach
combines automata and logics to tackle the challenges posed by diverse tree
data structures uniformly. At the core of our methodology is the knitted-tree
encoding, which maps a program execution into a tree data structure
encapsulating input, output, and intermediate configurations, within a single
structure. By leveraging the compositional properties of knitted-trees, we
characterize them using constrained Horn clauses (CHCs). This encoding reduces
verification to solving CHC satisfiability, benefiting from ongoing
advancements in CHC solvers. While we focus on the memory safety problem for
illustration, our technique applies broadly to various verification tasks
involving tree data structures.
🔗 View origin paper >>
Am I the publisher of this paper? I want to claim it
Claim
Paper Author: Marco Faella,Gennaro Parlato
Leave an answer
Hot post
Popular Paper