PV4 Symbolic Liveness Analysisdetects liveness violations

Detects liveness violations (e.g. infinite loops)

Application domain/field

Type of tool

Bug detector for liveness properties

Internals

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

Links

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

Last commit date

16 December 2021

Related papers

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

Last publication date

18 July 2018

ProVerB specific

View/edit source (Markdown)



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