Symbolic automatic relations and their applications to SMT and CHC solving

DOI10.1007/978-3-030-88806-0_20zbMath1497.68320arXiv2108.07642OpenAlexW3209569347MaRDI QIDQ2145347

Ryosuke Sato, Ken Sakayori, Naoki Kobayashi, Takumi Shimoda

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) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• IsaPlanner
• z3
• CVC4
• Rex
• Spacer

Cites Work

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

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