SMT-based BMC with function summarization based on Interpolation

 HiFrog as interpolating incremental C verifier offers support for the following features:

-- Various interpolants for QF_BOOL, QF-LRA, QF-UF

-- Injecting summaries ( User-Provided Summaries)

-- Automatic recursion unwinding

 -- Assertion optimization

-- Tuning the Strength of Summaries

--Tuning the Size of Summaries

-- Counterexamples

The architecture is depicted on the following diagram: