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|
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.