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

• Symbolic execution
• Incremental SAT solving
• Infeasibility checks

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.