PV3 Pinakachecks user-specified assertions in GOTO and C programs

Pinaka extends symbolic execution with incremental solving coupled with eager infeasibility checks

Application domain/field

Type of tool

Meant to be used in combination with CProver/Symex framework or maybe as a library?

Expected input

GOTO program or C program (which is translated into a GOTO program with the CProver/Symex framework)

Expected output

Successful/failed outcome (indicating an assertion violation) and a witness.

Internals

Pinaka is built on top of CProver+Symex framework. It uses incremental SAT solving, e.g. MiniSat, Glucose and MapleSAT.

Comments

The TACAS '19 paper mentions that Pinaka is the result of the rewriting and refactoring of VerifOx.
C

Links

Repository: https://github.com/sbjoshi/Pinaka

Related papers

Pinaka: Symbolic Execution Meets Incremental Solving (TACAS '19)

Last publication date

4 April 2019

ProVerB specific



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