PV4 Symbolic Liveness Analysisdetects liveness violations

Detects liveness violations (e.g. infinite loops)

Application domain/field

Type of tool

Bug detector for liveness properties


Symbolic Liveness Analysis was implemented as an extension of KLEE. It uses Z3.


Repository: https://github.com/COMSYS/SymbolicLivenessAnalysis

Related papers

https://doi.org/10.1007/978-3-319-96142-2_27 (CAV '18)

Last publication date

18 July 2018

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.