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

Last commit date

19 October 2020

Related papers

https://doi.org/10.1007/978-3-030-17502-3_20 (TACAS '19)

Last publication date

4 April 2019

ProVerB specific

View/edit source (Markdown)



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