Program
Verification
Book

PV4 ⊧ Symbolic Liveness Analysisdetects liveness violations

Detects liveness violations (e.g. infinite loops)

Application domain/field

Liveness properties
Symbolic execution
Bug detection

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: 15 Dec 2021 (default branch)
Last commit date: 16 Dec 2021 (last activity)

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.