Showing cs.PLShow all
2 papers · 1 filter
cs.PL2025
Verifying Tree-Manipulating Programs via CHCs
Marco Faella, Gennaro Parlato
Programs that manipulate tree-shaped data structures often require complex, specialized proofs that are difficult to generalize and automate. This paper introduces a unified, found…
cs.PL2024
Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
Marco Faella, Gennaro Parlato
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…