# Pinaka: Symbolic Execution meets Incremental Solving (Competition Contribution)

## TL;DR

Pinaka is a symbolic execution engine that leverages incremental SAT solving and eager infeasibility checks to efficiently analyze programs, demonstrating competitive performance in the SVCOMP 2019 competition.

## Contribution

It introduces a symbolic execution engine that integrates incremental SAT solving with configurable exploration strategies, enhancing efficiency over traditional methods.

## Key findings

- Supports both BFS and DFS strategies
- Uses partial incremental mode for improved performance
- Achieved competitive results in SVCOMP 2019

## Abstract

Many modern-day solvers offer functionality for incremental SAT solving, which preserves the state of the solver across invocations. This is beneficial when multiple, closely related SAT queries need to be fed to the solver. Pinaka is a symbolic execution engine which makes aggressive use of incremental SAT solving coupled with eager state infeasibility checks. It is built on top of the CProver/Symex framework. Pinaka supports both Breadth First Search and Depth First Search as state exploration strategies along with partial and full incremental modes. For SVCOMP 2019, Pinaka is configured to use partial incremental mode with Depth First Search strategy.