PV1 ⊧ FreqTermchecks whether the encoded program terminates

Application domain/field

• Program termination
• Syntax-guided synthesis (SyGuS)

Type of tool

Termination prover

Expected input

Program encoded as a system of linear constrained Horn clauses (CHCs).

Format:

? (Looks like SMT-LIB v2)

Expected output

terminates or unknown

Internals

Tool to prove program termination and non-termination using syntax-guided synthesis. Uses Spacer3, µZ AE-VAL, Z3. It is developed on top of FreqHorn.