3 papers
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.LO2024
A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version)
Marco Faella, Gennaro Parlato
We present a novel automata-based approach to address linear temporal logic modulo theory (LTL-MT) as a specification language for data words. LTL-MT extends LTL_f by replacing ato…