Reasoning About Data Trees Using CHCs

DOI10.1007/978-3-031-13188-2_13MaRDI QIDQ6487339zbMATH OpenFDO

Authors Marco Faella, Gennaro Parlato

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

Data structures (68P05) Logic in computer science (03B70)

Recommendations

• Decidable logics combining heap structures and data
• Logics for unordered trees with data constraints
• A decidable logic for tree data-structures with measurements
• Solving Horn clauses on inductive data types without induction
• Symbolic automatic relations and their applications to SMT and CHC solving

Cites work

• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 1158761 (Why is no real title available?)
• scientific article; zbMATH DE number 7440190 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• A constraint-based approach to solving games on infinite graphs
• An automata-theoretic approach to constraint LTL
• Automata and Logics for Words and Trees over an Infinite Alphabet
• Cinderella versus the wicked stepmother
• Combining decision procedures.
• Decidable logics combining heap structures and data
• Decision Problems of Finite Automata Design and Related Arithmetics
• Generalized finite automata theory with an application to a decision problem of second-order logic
• Horn clause solvers for program verification
• ICE-based refinement type discovery for higher-order functional programs
• Introduction to algorithms.
• Logics with rigidly guarded data tests
• Monadic second-order logic on finite sequences
• Qex: symbolic SQL query explorer
• Recursive proofs for inductive tree data-structures
• RustHorn: CHC-based verification for Rust programs
• Symbolic automatic relations and their applications to SMT and CHC solving
• Symbolic register automata
• Symbolic tree automata
• The Semantics of Predicate Logic as a Programming Language
• The tree width of auxiliary storage
• Tree acceptors and some of their applications
• Weak Second‐Order Arithmetic and Finite Automata

Cited in

(2)

• An efficient decision procedure for imperative tree data structures
• Symbolic automatic relations and their applications to SMT and CHC solving

This page was built for publication: Reasoning About Data Trees Using CHCs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6487339)