Pinaka
Verifier for C Programs
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.