Pinaka is single-path symbolic execution engine that makes use of eager infeasibility checks and incremental-solving.

Pinaka has been participating in an international software verification competition, SVCOMP, for the past 2 years. It is the first ever verifier from Indian academia to qualify in SVCOMP.

Here’s an overview of Pinaka’s performance (i.e the positions bagged in different categories).

Category SVCOMP 2019 SVCOMP 2020
ReachSafety - 8
-    ReachSafety-Floats 2 3
-    ReachSafety-Arrays 4 5
-    ReachSafety-Sequentialized - 5
-    ReachSafety-Recursive 8 9
-    ReachSafety-Heaps 9 10
Termination 8 6

Pinaka’s two strengths are speed and accuracy. If it produces an answer, it does so very fast. For example, in the ReachSafety-Floats subcategory, Pinaka was more than 10 times as fast as the verifier that stood first. Pinaka had 0 incorrect results in SVCOMP 2019, and only 3 in SVCOMP 2020 out of more than 4K benchmarks that it was run on.

Tool Tool Paper SVCOMP19 SVCOMP20