PV3 MSATIC3a dedicated property checker for infinite domains

Solver in nuXmv for infinite domains.

Internals

It is used as a back-end solver of nuXmv alongside MathSAT. The IC3 most likely refers to an incremental model checking algorithm for invariance properties.

Links

https://nuxmv.fbk.eu/downloads/nuxmv-user-manual.pdf

Related papers

https://doi.org/10.1007/978-3-030-25540-4_21 (CAV 2019)

Last publication date

2019

ProVerB specific

View/edit source (Markdown)



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