PV1 FreqTermchecks whether the encoded program terminates

Application domain/field

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 Spacer]3, µZ AE-VAL, Z3. It is developed on top of FreqHorn.
Termination

Links

Repository: https://github.com/grigoryfedyukovich/aeval/tree/term

Last commit date

10 February 2018

Related papers

https://doi.org/10.1007/978-3-319-96145-3_7

Last publication date

18 July 2018

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.