00000cab a22000003a 4500 UP-99796217608835423 Buklod 20231007234835.0 m |o d | ta 090519s xx d | ||r ||||| || DENGII eng Manevich, Roman PSE explaining program failures via postmortem static analysis. pp. 63-72 In this paper, we describe PSE (Postmortem Symbolic Evaluation), a static analysis algorithm that can be used by programmers to diagnose software failures. The algorithm requires minimal information about a failure, namely its kind (e.g. NULL dereference), and its location in the program's source code. It produces a set of execution traces along which the program can be driven to the given failure. PSE tracks the flow of a single value of interest from the point in the program where the failure occurred back to the points in the program where the value may have originated. The algorithm combines a novel dataflow analysis and memory alias analysis in a manner that allows for precise exploration of the program's behavior in polynomial time. We have applied PSE to the problem of diagnosing potential NULL-dereference errors in a suite of C programs, including several SPEC benchmarks and a large commercial operating system. In most cases, the analysis is able to either validate a pointer dereference, or find precise error traces demonstrating a NULL value for the pointer, in less than a second. Software. Software engineering. Software / Program Verification. Software engineering. Testing and debugging. Algorithms. Reliability. Security. Verification. Alias Analysis. Postmortem analysis. Typestate. Value flow. Software engineering notes. 29, 6 (2004). FO UPD DENG-II Article