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 ...

The colored graph isomorphism problem is a restricted version of the general graph isomorphism (GI)problem that involves deciding the existence of a color preserving isomorphism between a pair of colored graphs. In this ...

We present and solve a path optimization problem on programs. Given a set of program nodes, called critical nodes, we find a shortest path through the program's control flow graph that touches the maximum number of these ...

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 ...

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 ...

A dataflow query asks for the set of reachable (abstract) states, given a starting set of states. In this paper, we show how to optimize multiple queries on the same program (each with a different starting set of states) ...

In the modern world, not only is software getting larger and more complex, it is also becoming pervasive in our daily lives. On the one hand, the advent of multi-core processors is pushing software towards becoming more ...

This paper presents MCDASH, a refinement-based model checker for machine code. While model checkers such as SLAM, BLAST, and DASH have each made significant contributions in the field of verification/flaw-detection, ...

In this paper, we reduce pushdown system (PDS) model checking to a graph-theoretic problem, and apply a fast graph algorithm to improve the running time for model checking. We use \textit{weighted} PDSs as a generalized ...

Pushdown Systems (PDSs) are an important formalism for modeling programs. Reachability analysis on PDSs has been used extensively for program verification. A key result, which made PDSs popular in the model-checking ...