PV1 VeriAbs: Verification by Abstractionperforms several predefined analyses on C programs to make them compatible with a bounded model checker

VeriAbs verifies C programs by transforming them to abstract programs

Application domain/field

Model checking

Type of tool


Expected input

C program

Expected output

CBMC-compatible representation


C Model checking


Related papers

Last publication date

17 Apr 2020

Related tools

ProVerB specific

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