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

• SMT solving
• Quantified formula
• Model generation
• Quantifier elimination

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