Automating induction for solving Horn clauses

DOI10.1007/978-3-319-63390-9_30MaRDI QIDQ2164260zbMATH OpenOpenAlexFDO

Authors Hiroshi Unno, Sho Torii, Hiroki Sakamoto

Publication date 12 August 2022

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: Verification problems of programs written in various paradigms (such as imperative, logic, concurrent, functional, and object-oriented ones) can be reduced to problems of solving Horn clause constraints on predicate variables that represent unknown inductive invariants. This paper presents a novel Horn constraint solving method based on inductive theorem proving: the method reduces Horn constraint solving to validity checking of first-order formulas with inductively defined predicates, which are then checked by induction on the derivation of the predicates. To automate inductive proofs, we introduce a novel proof system tailored to Horn constraint solving and use an SMT solver to discharge proof obligations arising in the proof search. The main advantage of the proposed method is that it can verify relational specifications across programs in various paradigms where multiple function calls need to be analyzed simultaneously. The class of specifications includes practically important ones such as functional equivalence, associativity, commutativity, distributivity, monotonicity, idempotency, and non-interference. Furthermore, our novel combination of Horn clause constraints with inductive theorem proving enables us to naturally and automatically axiomatize recursive functions that are possibly non-terminating, non-deterministic, higher-order, exception-raising, and over non-inductively defined data types. We have implemented a relational verification tool for the OCaml functional language based on the proposed method and obtained promising results in preliminary experiments.

Recommendations

• Horn clause solvers for program verification
• Solving Horn clauses on inductive data types without induction
• Relational verification through Horn clause transformation
• Constraint-based relational verification
• Probabilistic Horn clause verification

Cited in

(30)

• Inferring simple solutions to recursion-free Horn clauses via sampling
• Synchronizing constrained Horn clauses
• Constraint-based relational verification
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• Automating Induction with an SMT Solver
• scientific article; zbMATH DE number 7453193 (Why is no real title available?)
• Autark assignments of Horn CNFs
• Unbounded procedure summaries from bounded environments
• HoIce: an ICE-based non-linear Horn clause solver
• Horn clause solvers for program verification
• Catamorphic abstractions for constrained Horn clause satisfiability
• scientific article; zbMATH DE number 7806141 (Why is no real title available?)
• Solving constrained Horn clauses over algebraic data types
• Symbolic automatic relations and their applications to SMT and CHC solving
• Bridging arrays and ADTs in recursive proofs
• Loop verification with invariants and contracts
• Asynchronous unfold/fold transformation for fixpoint logic
• scientific article; zbMATH DE number 7444023 (Why is no real title available?)
• Relational verification via invariant-guided synchronization
• Relational verification through Horn clause transformation
• Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
• A fixed-point theorem for Horn formula equations
• On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs
• An abstract fixed-point theorem for Horn formula equations
• Temporal verification of programs via first-order fixpoint logic
• Relational cost analysis in a functional-imperative setting
• Solving Horn clauses on inductive data types without induction
• Fold/unfold transformations for fixpoint logic
• Removing algebraic data types from constrained Horn clauses using difference predicates
• Horn clause verification with convex polyhedral abstraction and tree automata-based refinement

This page was built for publication: Automating induction for solving Horn clauses

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