Name
Abstract | ||
|---|---|---|
Detecting infeasible paths (IFPs) allows accurate computation of various kinds of program slices, and accurate detection of semantic errors that may occur when two variants of a program are merged. We propose a method of efficiently determining the truth of a prenex normal form Presburger sentence (P-sentence) bounded only by existential quantifiers, which is suitable for detecting IFPs. In this method, a coefficients matrix is converted into a triangular matrix based on the method proposed by D.C. Cooper. If the rank of the matrix is lower than the degree of the matrix, the matrix is triangulated by using a method for solving one linear equation with three or more unknowns, so that the matrix can be back-substituted. This paper also reports that an implementation of our method shows a slower increase in computation time than the previous method and reduces computation time by up to 3,000,000 times. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1002/(SICI)1520-684X(199908)30:9<74::AID-SCJ9>3.0.CO;2-# | Systems and Computers in Japan |
Keywords | Field | DocType |
accurate computation,program slice,computation time,previous method,d.c. cooper,existential quantifiers,infeasible path,accurate detection,triangular matrix,presburger arithmetic,coefficients matrix,prototypes,linear equations,computation,program slicing,arithmetic,linear equation,formal logic,computational complexity,normal form | Linear equation,Computer science,Matrix (mathematics),Prenex normal form,Algorithm,Presburger arithmetic,Gaussian elimination,Triangular matrix,Computational complexity theory,Computation | Journal |
Volume | Issue | Citations |
30 | 9 | 1 |
PageRank | References | Authors |
0.63 | 13 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kuniaki Naoi | 1 | 5 | 2.44 |
| Naohisa Takahashi | 2 | 123 | 27.99 |