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)

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.

[error in script]

IITH Creators:	IITH Creators ORCiD Joshi, Saurabh UNSPECIFIED
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
URI:	http://raiithold.iith.ac.in/id/eprint/5136
Publisher URL:	http://doi.org/10.1007/978-3-030-17502-3_20
Related URLs:	Google Scholar

Actions (login required)

View Item

Statistics for this ePrint Item