In recent years, the use of symbolic analysis in systems for testing and verifying programs has experienced a resurgence. By ``symbolic program analysis'', we mean logic-based techniques to analyze state changes along ...

We consider the model-checking problem for C programs with (1) data ranging over very large domains, (2) (recursive) procedure calls, and (3) concurrent parallel components that communicate via synchronizing actions. We ...

This paper addresses two problems that arise when analyzing executables: (1) recovering variable-like quantities in the absence of symbol-table and debugging information, and (2) recovering useful information about objects ...

We present a new decision procedure for detecting property violations in pushdown models for concurrent programs that use lock-based synchronization, where each thread's lock operations are properly nested (a la ...

In this paper, we present an abstraction for heap-allocated storage, called the recency-abstraction, that allows abstract-interpretation algorithms to recover non-trivial information for heap-allocated data objects. As an ...

This paper addresses the analysis of concurrent programs with shared memory. Such an analysis is undecidable in the presence of multiple procedures. One approach used in recent work obtains decidability by providing only ...

This paper concerns the question of how to create abstractions that are useful for program analysis. It presents a method that refines an abstraction automatically for analysis problems in which the semantics of statements ...

There is growing interest in analyzing executables to look for bugs and security vulnerabilities. This paper describes the design and implementation of a language for describing the semantics of an instruction set, along ...

We present a numeric analysis that is capable of reasoning about array operations. In particular, the analysis is able to establish that all elements of an array have been initialized ("an array kill"), as well as to ...

Extended weighted pushdown systems (EWPDSs) are an extension of pushdown systems that incorporate infinite-state data abstractions. Nested-word automata (NWAs) are able to recognize languages that exhibit context-free ...