Pinaka: Symbolic Execution Meets Incremental Solving

Chaudhary, Eti and Joshi, Saurabh (2019) Pinaka: Symbolic Execution Meets Incremental Solving. In: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS, 6-11 April 2019, Prague, Czech Republic.

Full text not available from this repository. (Request a copy)


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.

[error in script]
IITH Creators:
IITH CreatorsORCiD
Item Type: Conference or Workshop Item (Paper)
Uncontrolled Keywords: Incremental solving, Software bug detection, Symbolic execution
Subjects: Computer science
Divisions: Department of Computer Science & Engineering
Depositing User: Team Library
Date Deposited: 13 May 2019 07:40
Last Modified: 13 May 2019 07:40
Publisher URL:
Related URLs:

Actions (login required)

View Item View Item
Statistics for RAIITH ePrint 5136 Statistics for this ePrint Item