PV2 TFML: Taint engine for ForMuLagenerates a quantifier-free formula overapproximating a given quantified formula

Tool to generate models of quantified first-order formula over built-in theories

Application domain/field

Type of tool

Meta-tool?

Expected input

Quantified SMT formula

Format:

SMT-LIB (ABV, arrays and bitvectors, theory)

Expected output

SMT-LIB formula

Internals

They focus on the problem to generate models (i.e. find solutions) of an SMT formula. Given a quantified formula, they transform it into a quantifier-free formula with the guarantee that any model of the latter contains a model of the former.

Comments

License: GNU LGPL v2.1
SMT

Links

Last commit date

27 August 2018

Related papers

https://doi.org/10.1007/978-3-319-96142-2_19 (CAV 2018)

Last publication date

18 July 2018

Related tools

BINSEC

ProVerB specific

View/edit source (Markdown)



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