PV4 Uniquegenerates interpolant graphs from CNF formulae

Application domain/field

Expected input

Expected output

Internals

Uses ItpMiniSat, a modified version of MiniSat, bundled with the ExtAvy model checker

Links

https://github.com/fslivovsky/unique

Last commit date

23 April 2022

Related papers

https://doi.org/10.1007/978-3-030-53288-8_24 (CAV '20)

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



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