Automatic Inference of Recursive Invariants Based on Catamorphisms

Motivation

Invariant leads to exclude entire state spaces which helps with analysis of static analysis programs.

Features

• fully automatic inference of inductive invariant
• support data structures
• representation of inductive invariant
• support SMT theory combination

How to use

Clone submodules

git clone --recursive https://github.com/ndreuu/SMTLIB2.git
git submodule update --init --recursive 

Run

cd /CataHornSolver
dotnet run <path-to-chc.smt2>

Contacts

email: a.oleyn1kov@outlook.com