Symbolic automatic relations and their applications to SMT and CHC solving

DOI10.1007/978-3-030-88806-0_20zbMATH Open1497.68320arXiv2108.07642OpenAlexW3209569347MaRDI QIDQ2145347FDOQ2145347

Ryosuke Sato, Ken Sakayori, Naoki Kobayashi, Takumi Shimoda

Publication date: 17 June 2022

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.

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)

Cites Work

• Isabelle. A generic theorem prover
• Title not available (Why is that?)
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• Extended symbolic finite automata and transducers
• Verification, Model Checking, and Abstract Interpretation
• Symbolic Automata Constraint Solving
• SMT-based model checking for recursive programs
• The power of symbolic automata and transducers
• Automating induction for solving Horn clauses
• Horn Clause Solvers for Program Verification
• Case-Analysis for Rippling and Inductive Proof
• Automatic presentations of structures
• Qex: Symbolic SQL Query Explorer
• Title not available (Why is that?)
• Removing algebraic data types from constrained Horn clauses using difference predicates
• Solving Horn Clauses on Inductive Data Types Without Induction
• Bridging arrays and ADTs in recursive proofs
• Compositional and Lightweight Dependent Type Inference for ML
• Automatic Structures
• ICE-based refinement type discovery for higher-order functional programs

Cited In (2)

• Reasoning About Data Trees Using CHCs
• Neural network-guided synthesis of recursive list functions

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)