Reasoning About Data Trees Using CHCs

DOI10.1007/978-3-031-13188-2_13zbMATH Open1514.68045MaRDI QIDQ6487339FDOQ6487339

Authors: Marco Faella, Gennaro Parlato 

Publication date: 7 December 2022

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

Mathematics Subject Classification ID

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

Cites Work

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

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)