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

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) 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)

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

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)