26 citations · 26 across the 4 of their papers we have counts for
Showing cs.PLShow all
3 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…
cs.PL2013
Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists
Pranav Garg, P. Madhusudan, Gennaro Parlato
We propose a new approach to heap analysis through an abstract domain of automata, called automatic shapes. The abstract domain uses a particular kind of automata, called quantifie…