Symbolic automatic relations and their applications to SMT and CHC solving

DOI10.1007/978-3-030-88806-0_20MaRDI QIDQ2145347zbMATHOpenAlexFDO

Authors Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato

Publication date 17 June 2022

Full work available at URL https://arxiv.org/abs/2108.07642

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers. To address the challenge, we introduce the notion of symbolic automatic relations (SARs), which combines symbolic automata and automatic relations, and inherits their good properties such as the closure under Boolean operations. We consider the satisfiability problem for SARs, and show that it is undecidable in general, but that we can construct a sound (but incomplete) and automated satisfiability checker by a reduction to CHC solving. We discuss applications to SMT and CHC solving on data structures, and show the effectiveness of our approach through experiments.

Recommendations

• Reasoning About Data Trees Using CHCs
• SMT-based model checking for recursive programs
• Symbolic automata constraint solving
• Taking satisfiability to the next level with Z3 (abstract)
• Solving Horn clauses on inductive data types without induction

Cites work

• scientific article; zbMATH DE number 3466489 (Why is no real title available?)
• An abstract decision procedure for a theory of inductive data types.
• Automatic presentations of structures
• Automatic structures: twenty years later
• Automating induction for solving Horn clauses
• Bridging arrays and ADTs in recursive proofs
• Case-analysis for rippling and inductive proof
• Compositional and lightweight dependent type inference for ML
• Extended symbolic finite automata and transducers
• Horn clause solvers for program verification
• ICE-based refinement type discovery for higher-order functional programs
• Isabelle. A generic theorem prover
• Qex: symbolic SQL query explorer
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• Removing algebraic data types from constrained Horn clauses using difference predicates
• SMT-based model checking for recursive programs
• Solving Horn clauses on inductive data types without induction
• Symbolic automata constraint solving
• The power of symbolic automata and transducers
• Verification, Model Checking, and Abstract Interpretation

Cited in

(3)

• Reasoning About Data Trees Using CHCs
• Neural network-guided synthesis of recursive list functions
• Bridging arrays and ADTs in recursive proofs

Describes a project that uses

Uses Software

• IsaPlanner
• z3
• CVC4
• Rex
• Spacer

This page was built for publication: Symbolic automatic relations and their applications to SMT and CHC solving

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