Infeasible Code Detection
Date
2012
Authors
Bertolini, Cristiano
Schäf, Martin
Schweitzer, Pascal
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
Abstract
A piece of code in a computer program is infeasible if it cannot be part of any normally-terminating execution of the program. We develop an algorithm for the automatic detection of all infeasible code in a program. We first translate the task of determining all infeasible code into the problem of finding all statements that can be covered by a feasible path. We prove that in order to identify all coverable statements, it is sufficient to find all coverable statements within a certain minimal subset. For this, our algorithm repeatedly queries an oracle, asking for the infeasibility of specific sets of control-flow paths. We present a sound implementation of the proposed algorithm on top of the Boogie program verifier utilizing a theorem prover to provide the oracle required by the algorithm. We show experimentally a drastic decrease in the number of theorem prover queries compared to existing approaches, resulting in an overall speedup of the entire computation.
Description
Keywords
Keywords: Automatic Detection; Code detection; Computer program; Control-flow; Coverable; Minimal subset; Program verifiers; Theorem provers; Codes (symbols); Experiments; Algorithms
Citation
Collections
Source
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31
Downloads
File
Description